theorem :: YELLOW10:64

for S, T being antisymmetric bounded with_suprema with_infima RelStr st [:S,T:] is complemented holds
( S is complemented & T is complemented )