theorem :: YELLOW10:54

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