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