set IT = Y |^ X;
let x, y be Element of (Y |^ X); :: according to LATTICE3:def 10 :: thesis:
reconsider x' = x as Function of X,the carrier of Y by Lm5;
reconsider y' = y as Function of X,the carrier of Y by Lm5;
defpred S₁[ set , set ] means ex xa, ya being Element of Y st
( xa = x' . X & ya = y' . X & Y = xa "\/" ya );
A1: for x being set st x in X holds
ex y being set st
( y in the carrier of Y & S₁[x,y] )

proof

let a be set ; :: thesis:
assume a in X ; :: thesis:
then reconsider xa = x' . a, ya = y' . a as Element of Y by FUNCT_2:7;
take y = xa "\/" ya; :: thesis:
thus y in the carrier of Y ; :: thesis:
take xa ; :: thesis:
take ya ; :: thesis:
thus ( xa = x' . a & ya = y' . a & y = xa "\/" ya ) ; :: thesis:

end;

consider f being Function of X,the carrier of Y such that
A2: for a being set st a in X holds
S₁[a,f . a] from FUNCT_2:sch 1(A1);
f in Funcs X,the carrier of Y by FUNCT_2:11;
then reconsider z = f as Element of (Y |^ X) by Th28;
take z ; :: thesis:
A3: x <= z

proof

reconsider x1 = x, z1 = z as Element of (product (X --> Y)) ;
x1 in the carrier of (product (X --> Y)) ;
then A4: x1 in product (Carrier (X --> Y)) by Def4;
ex f, g being Function st
( f = x1 & g = z1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )

proof

take x' ; :: thesis:
take f ; :: thesis:
thus ( x' = x1 & f = z1 ) ; :: thesis:
let i be set ; :: thesis:
assume i in X ; :: thesis:
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
A5: R = Y by FUNCOP_1:13;
reconsider yi = f . i, xi = x' . i as Element of R by FUNCOP_1:13;
take R ; :: thesis:
take xi ; :: thesis:
take yi ; :: thesis:
consider xa, ya being Element of Y such that
A6: ( xa = x' . i & ya = y' . i & f . i = xa "\/" ya ) by A2;
thus ( R = (X --> Y) . i & xi = x' . i & yi = f . i & xi <= yi ) by A5, A6, YELLOW_0:22; :: thesis:

end;

hence x <= z by A4, Def4; :: thesis:

end;

A7: y <= z

proof

reconsider y1 = y, z1 = z as Element of (product (X --> Y)) ;
y1 in the carrier of (product (X --> Y)) ;
then A8: y1 in product (Carrier (X --> Y)) by Def4;
ex f, g being Function st
( f = y1 & g = z1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )

proof

take y' ; :: thesis:
take f ; :: thesis:
thus ( y' = y1 & f = z1 ) ; :: thesis:
let i be set ; :: thesis:
assume i in X ; :: thesis:
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
A9: R = Y by FUNCOP_1:13;
reconsider yi = f . i, xi = y' . i as Element of R by FUNCOP_1:13;
take R ; :: thesis:
take xi ; :: thesis:
take yi ; :: thesis:
consider xa, ya being Element of Y such that
A10: ( xa = x' . i & ya = y' . i & f . i = xa "\/" ya ) by A2;
thus ( R = (X --> Y) . i & xi = y' . i & yi = f . i & xi <= yi ) by A9, A10, YELLOW_0:22; :: thesis:

end;

hence y <= z by A8, Def4; :: thesis:

end;

for z' being Element of (Y |^ X) st z' >= x & z' >= y holds
z' >= z

proof

let z' be Element of (Y |^ X); :: thesis:
assume A11: ( z' >= x & z' >= y ) ; :: thesis:
z' >= z

proof

reconsider z2 = z', z3 = z, z4 = y, z5 = x as Element of (product (X --> Y)) ;
reconsider K = z3, J = z2 as Function of X,the carrier of Y by Lm5;
( z5 in the carrier of (product (X --> Y)) & z3 in the carrier of (product (X --> Y)) & z4 in the carrier of (product (X --> Y)) ) ;
then A12: ( z5 in product (Carrier (X --> Y)) & z3 in product (Carrier (X --> Y)) & z4 in product (Carrier (X --> Y)) ) by Def4;
then consider f1, g1 being Function such that
A13: ( f1 = z5 & g1 = z2 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f1 . i & yi = g1 . i & xi <= yi ) ) ) by A11, Def4;
consider f2, g2 being Function such that
A14: ( f2 = z4 & g2 = z2 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) ) ) by A11, A12, Def4;
ex f, g being Function st
( f = z3 & g = z2 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )

proof

take K ; :: thesis:
take J ; :: thesis:
thus ( K = z3 & J = z2 ) ; :: thesis:
let i be set ; :: thesis:
assume i in X ; :: thesis:
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
A15: R = Y by FUNCOP_1:13;
reconsider yi = J . i, xi = K . i as Element of R by FUNCOP_1:13;
take R ; :: thesis:
take xi ; :: thesis:
take yi ; :: thesis:
consider xa, ya being Element of Y such that
A16: ( xa = x' . i & ya = y' . i & f . i = xa "\/" ya ) by A2;
consider R1 being RelStr , xi1, yi1 being Element of R1 such that
A17: ( R1 = (X --> Y) . i & xi1 = f1 . i & yi1 = g1 . i & xi1 <= yi1 ) by A13;
consider R2 being RelStr , xi2, yi2 being Element of R2 such that
A18: ( R2 = (X --> Y) . i & xi2 = f2 . i & yi2 = g2 . i & xi2 <= yi2 ) by A14;
thus ( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi ) by A13, A14, A15, A16, A17, A18, YELLOW_0:22; :: thesis:

end;

hence z' >= z by A12, Def4; :: thesis:

end;

hence z' >= z ; :: thesis:

end;

hence ( x <= z & y <= z & ( for b₁ being Element of the carrier of (Y |^ X) holds
( not x <= b₁ or not y <= b₁ or z <= b₁ ) ) ) by A3, A7; :: thesis: