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