theorem :: WAYBEL_2:11

for S, T being non empty reflexive antisymmetric RelStr st [:S,T:] is up-complete holds
( S is up-complete & T is up-complete )