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