theorem :: YELLOW10:59

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 is directly_closed & Y is directly_closed holds
[:X,Y:] is directly_closed