theorem :: YELLOW10:7

for S, T being non empty RelStr
for x, y being Element of [:S,T:] holds
( x is_<=_than {y} iff ( x `1 is_<=_than {(y `1)} & x `2 is_<=_than {(y `2)} ) )