let S, T be non empty RelStr ; :: thesis: 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 )} ) )
let x, y be Element of [:S,T:]; :: thesis: ( x is_>=_than {y} iff ( x `1 is_>=_than {(y `1 )} & x `2 is_>=_than {(y `2 )} ) )
thus ( x is_>=_than {y} implies ( x `1 is_>=_than {(y `1 )} & x `2 is_>=_than {(y `2 )} ) ) :: thesis: ( x `1 is_>=_than {(y `1 )} & x `2 is_>=_than {(y `2 )} implies x is_>=_than {y} )

proof

A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2;
then A2: x = [(x `1 ),(x `2 )] by MCART_1:23;
y = [(y `1 ),(y `2 )] by A1, MCART_1:23;
then A3: [(y `1 ),(y `2 )] in {y} by TARSKI:def 1;
assume for b being Element of [:S,T:] st b in {y} holds
x >= b ; :: according to LATTICE3:def 9 :: thesis: ( x `1 is_>=_than {(y `1 )} & x `2 is_>=_than {(y `2 )} )
then A4: x >= [(y `1 ),(y `2 )] by A3;

hereby :: according to LATTICE3:def 9 :: thesis: x `2 is_>=_than {(y `2 )}

let b be Element of S; :: thesis: ( b in {(y `1 )} implies x `1 >= b )
assume b in {(y `1 )} ; :: thesis: x `1 >= b
then b = y `1 by TARSKI:def 1;
hence x `1 >= b by A4, A2, YELLOW_3:11; :: thesis: verum

end;

let b be Element of T; :: according to LATTICE3:def 9 :: thesis: ( not b in {(y `2 )} or b <= x `2 )
assume b in {(y `2 )} ; :: thesis: b <= x `2
then b = y `2 by TARSKI:def 1;
hence b <= x `2 by A4, A2, YELLOW_3:11; :: thesis: verum

end;

assume that
A5: for b being Element of S st b in {(y `1 )} holds
x `1 >= b and
A6: for b being Element of T st b in {(y `2 )} holds
x `2 >= b ; :: according to LATTICE3:def 9 :: thesis: x is_>=_than {y}
let b be Element of [:S,T:]; :: according to LATTICE3:def 9 :: thesis: ( not b in {y} or b <= x )
assume b in {y} ; :: thesis: b <= x
then A7: b = y by TARSKI:def 1;
then b `2 in {(y `2 )} by TARSKI:def 1;
then A8: x `2 >= b `2 by A6;
b `1 in {(y `1 )} by A7, TARSKI:def 1;
then x `1 >= b `1 by A5;
hence b <= x by A8, YELLOW_3:12; :: thesis: verum