theorem :: YELLOW10:63

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