theorem :: YELLOW_3:45

for X, Y being non empty antisymmetric lower-bounded RelStr st [:X,Y:] is complete holds
( X is complete & Y is complete )