theorem Th12: :: YELLOW_3:12

for S1, S2 being non empty RelStr
for x, y being Element of [:S1,S2:] holds
( x <= y iff ( x `1 <= y `1 & x `2 <= y `2 ) )