set IT = Y |^ X;
let x, y be Element of (Y |^ X); :: according to LATTICE3:def 10 :: thesis:
reconsider y' = y as Function of X,the carrier of Y by Lm5;
reconsider x' = x 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: y <= z

proof

reconsider y1 = y, z1 = z as Element of (product (X --> Y)) ;
A4: 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 ;
reconsider yi = f . i, xi = y' . i as Element of R by FUNCOP_1:13;
take R ; :: thesis:
take xi ; :: thesis:
take yi ; :: thesis:
( R = Y & ex xa, ya being Element of Y st
( xa = x' . i & ya = y' . i & f . i = xa "\/" ya ) ) by A2, FUNCOP_1:13;
hence ( R = (X --> Y) . i & xi = y' . i & yi = f . i & xi <= yi ) by YELLOW_0:22; :: thesis:

end;

y1 in the carrier of (product (X --> Y)) ;
then y1 in product (Carrier (X --> Y)) by Def4;
hence y <= z by A4, Def4; :: thesis:

end;

A5: 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 that
A6: z' >= x and
A7: z' >= y ; :: thesis:
z' >= z

proof

reconsider z2 = z', z3 = z, z4 = y, z5 = x as Element of (product (X --> Y)) ;
z4 in the carrier of (product (X --> Y)) ;
then z4 in product (Carrier (X --> Y)) by Def4;
then consider f2, g2 being Function such that
A8: ( f2 = z4 & g2 = z2 ) and
A9: 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 A7, Def4;
reconsider K = z3, J = z2 as Function of X,the carrier of Y by Lm5;
z5 in the carrier of (product (X --> Y)) ;
then z5 in product (Carrier (X --> Y)) by Def4;
then consider f1, g1 being Function such that
A10: ( f1 = z5 & g1 = z2 ) and
A11: 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 A6, Def4;
A12: 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 ;
reconsider yi = J . i, xi = K . i as Element of R by FUNCOP_1:13;
take R ; :: thesis:
take xi ; :: thesis:
take yi ; :: thesis:
A13: ( R = Y & ex xa, ya being Element of Y st
( xa = x' . i & ya = y' . i & f . i = xa "\/" ya ) ) by A2, FUNCOP_1:13;
( ex R1 being RelStr ex xi1, yi1 being Element of R1 st
( R1 = (X --> Y) . i & xi1 = f1 . i & yi1 = g1 . i & xi1 <= yi1 ) & ex R2 being RelStr ex xi2, yi2 being Element of R2 st
( R2 = (X --> Y) . i & xi2 = f2 . i & yi2 = g2 . i & xi2 <= yi2 ) ) by A11, A9;
hence ( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi ) by A10, A8, A13, YELLOW_0:22; :: thesis:

end;

z3 in the carrier of (product (X --> Y)) ;
then z3 in product (Carrier (X --> Y)) by Def4;
hence z' >= z by A12, Def4; :: thesis:

end;

hence z' >= z ; :: thesis:

end;

x <= z

proof

reconsider x1 = x, z1 = z as Element of (product (X --> Y)) ;
A14: 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 ;
reconsider yi = f . i, xi = x' . i as Element of R by FUNCOP_1:13;
take R ; :: thesis:
take xi ; :: thesis:
take yi ; :: thesis:
( R = Y & ex xa, ya being Element of Y st
( xa = x' . i & ya = y' . i & f . i = xa "\/" ya ) ) by A2, FUNCOP_1:13;
hence ( R = (X --> Y) . i & xi = x' . i & yi = f . i & xi <= yi ) by YELLOW_0:22; :: thesis:

end;

x1 in the carrier of (product (X --> Y)) ;
then x1 in product (Carrier (X --> Y)) by Def4;
hence x <= z by A14, Def4; :: 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, A5; :: thesis: