let S, T be 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)} ) )
let x, y, z be Element of [:S,T:]; ( 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)} ) )
( 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
;
LATTICE3:def 9 ( 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;
let b be
Element of
T;
LATTICE3:def 9 ( not b in {(y `2),(z `2)} or b <= x `2 )
assume
b in {(y `2),(z `2)}
;
b <= x `2
then
(
b = y `2 or
b = z `2 )
by TARSKI:def 2;
hence
b <= x `2
by A3, A4, A5, YELLOW_3:11;
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
; LATTICE3:def 9 x is_>=_than {y,z}
let b be Element of [:S,T:]; LATTICE3:def 9 ( not b in {y,z} or b <= x )
assume
b in {y,z}
; b <= x
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
b <= x
by A9, YELLOW_3:12; verum