theorem :: YELLOW10:10

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