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