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 )] &
z = [(z `1 ),(z `2 )] )
by MCART_1:23;
then
(
[(y `1 ),(y `2 )] in {y,z} &
[(z `1 ),(z `2 )] in {y,z} )
by TARSKI:def 2;
then A3:
(
x <= [(y `1 ),(y `2 )] &
x <= [(z `1 ),(z `2 )] )
by A1;
A4:
x = [(x `1 ),(x `2 )]
by A2, MCART_1:23;
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, YELLOW_3:11;
:: thesis: verum
end;
assume that
A5:
for b being Element of S st b in {(y `1 ),(z `1 )} holds
x `1 <= b
and
A6:
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
( b = y or b = z )
by TARSKI:def 2;
then
( b `1 in {(y `1 ),(z `1 )} & b `2 in {(y `2 ),(z `2 )} )
by TARSKI:def 2;
then
( x `1 <= b `1 & x `2 <= b `2 )
by A5, A6;
hence
x <= b
by YELLOW_3:12; :: thesis: verum