RBOX:
	INCLUSION(R, S)
TBOX:
	INCLUSION(A, LEQ(01, S, TOP))
	INCLUSION(A, EXISTS(R, TOP))
ABOX:
	a : EXISTS(S-, A)
END