set IT = Y |^ X;
let x, y be Element of (Y |^ X); :: according to LATTICE3:def 11 :: 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: z <= x

proof

reconsider x1 = x, z1 = z as Element of (product (X --> Y)) ;
z1 in the carrier of (product (X --> Y)) ;
then A4: z1 in product (Carrier (X --> Y)) by Def4;
ex f, g being Function st
( f = z1 & g = x1 & ( 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 f ; :: thesis:
take x' ; :: thesis:
thus ( f = z1 & x' = x1 ) ; :: 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 xi = f . i, yi = 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 = f . i & yi = x' . i & xi <= yi ) by A5, A6, YELLOW_0:23; :: thesis:

end;

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

end;

A7: z <= y

proof

reconsider y1 = y, z1 = z as Element of (product (X --> Y)) ;
z1 in the carrier of (product (X --> Y)) ;
then A8: z1 in product (Carrier (X --> Y)) by Def4;
ex f, g being Function st
( f = z1 & g = y1 & ( 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 f ; :: thesis:
take y' ; :: thesis:
thus ( f = z1 & y' = y1 ) ; :: 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 xi = f . i, yi = 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 = f . i & yi = y' . i & xi <= yi ) by A9, A10, YELLOW_0:23; :: thesis:

end;

hence z <= y 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 J = z2, K = z3 as Function of X,the carrier of Y by Lm5;
z' in the carrier of (product (X --> Y)) ;
then A12: z2 in product (Carrier (X --> Y)) by Def4;
then consider f1, g1 being Function such that
A13: ( f1 = z2 & g1 = z5 & ( 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 = z2 & g2 = z4 & ( 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 = z2 & g = z3 & ( 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 J ; :: thesis:
take K ; :: thesis:
thus ( J = z2 & K = z3 ) ; :: 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 xi = J . i, yi = 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 = J . i & yi = K . i & xi <= yi ) by A13, A14, A15, A16, A17, A18, YELLOW_0:23; :: thesis:

end;

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

end;

hence z' <= z ; :: thesis:

end;

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