theorem Th31: :: YELLOW_3:31

for S1, S2 being non empty RelStr
for D being Subset of [:S1,S2:]
for x being Element of S1
for y being Element of S2 holds
( [x,y] is_>=_than D iff ( x is_>=_than proj1 D & y is_>=_than proj2 D ) )