theorem :: YELLOW10:58

for S, T being non empty reflexive antisymmetric up-complete RelStr
for X being Subset of S
for Y being Subset of T st [:X,Y:] is directly_closed holds
( ( Y <> {} implies X is directly_closed ) & ( X <> {} implies Y is directly_closed ) )