theorem :: YELLOW10:60

for S, T being non empty reflexive antisymmetric up-complete RelStr
for X being Subset of [:S,T:] st X is property(S) holds
( proj1 X is property(S) & proj2 X is property(S) )