set IT = [:X,Y:];
let x, y be Element of [:X,Y:]; :: according to LATTICE3:def 11 :: thesis: ex b₁ being Element of the carrier of [:X,Y:] st
( b₁ <= x & b₁ <= y & ( for b₂ being Element of the carrier of [:X,Y:] holds
( not b₂ <= x or not b₂ <= y or b₂ <= b₁ ) ) )
consider zx being Element of X such that
A1: ( x `1 >= zx & y `1 >= zx ) and
A2: for z' being Element of X st x `1 >= z' & y `1 >= z' holds
zx >= z' by LATTICE3:def 11;
consider zy being Element of Y such that
A3: ( x `2 >= zy & y `2 >= zy ) and
A4: for z' being Element of Y st x `2 >= z' & y `2 >= z' holds
zy >= z' by LATTICE3:def 11;
A5: the carrier of [:X,Y:] = [:the carrier of X,the carrier of Y:] by Def2;
then consider a, b being set such that
A6: ( a in the carrier of X & b in the carrier of Y & x = [a,b] ) by ZFMISC_1:def 2;
consider c, d being set such that
A7: ( c in the carrier of X & d in the carrier of Y & y = [c,d] ) by A5, ZFMISC_1:def 2;
take z = [zx,zy]; :: thesis: ( z <= x & z <= y & ( for b₁ being Element of the carrier of [:X,Y:] holds
( not b₁ <= x or not b₁ <= y or b₁ <= z ) ) )
( [(x `1 ),(x `2 )] >= [zx,zy] & [(y `1 ),(y `2 )] >= [zx,zy] ) by A1, A3, Th11;
hence ( x >= z & y >= z ) by A6, A7, MCART_1:8; :: thesis: for b₁ being Element of the carrier of [:X,Y:] holds
( not b₁ <= x or not b₁ <= y or b₁ <= z )
let z' be Element of [:X,Y:]; :: thesis: ( not z' <= x or not z' <= y or z' <= z )
consider a, b being set such that
A8: ( a in the carrier of X & b in the carrier of Y & z' = [a,b] ) by A5, ZFMISC_1:def 2;
assume ( x >= z' & y >= z' ) ; :: thesis: z' <= z
then ( x `1 >= z' `1 & x `2 >= z' `2 & y `1 >= z' `1 & y `2 >= z' `2 ) by Th12;
then ( zx >= z' `1 & zy >= z' `2 ) by A2, A4;
then [zx,zy] >= [(z' `1 ),(z' `2 )] by Th11;
hence z' <= z by A8, MCART_1:8; :: thesis: verum