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

proof

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

hereby :: according to LATTICE3:def 8 :: thesis: x `2 is_<=_than {(y `2),(z `2)}

let b be Element of S; :: thesis: ( b in {(y `1),(z `1)} implies x `1 <= b )
assume b in {(y `1),(z `1)} ; :: thesis: x `1 <= b
then ( b = y `1 or b = z `1 ) by TARSKI:def 2;
hence x `1 <= b by A3, A4, A5, YELLOW_3:11; :: thesis: verum

end;

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

end;

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