theorem :: YELLOW10:9

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)} ) )