set IT = Y |^ X;
let x, y be Element of (Y |^ X); :: according to LATTICE3:def 10 :: thesis: ex b1 being Element of the carrier of (Y |^ X) st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of (Y |^ X) holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
reconsider y9 = y as Function of X, the carrier of Y by Lm5;
reconsider x9 = x as Function of X, the carrier of Y by Lm5;
defpred S1[ object , object ] means ex xa, ya being Element of Y st
( xa = x9 . X & ya = y9 . X & Y = xa "\/" ya );
A1: for x being object st x in X holds
ex y being object st
( y in the carrier of Y & S1[x,y] )
proof
let a be object ; :: thesis: ( a in X implies ex y being object st
( y in the carrier of Y & S1[a,y] ) )
assume a in X ; :: thesis: ex y being object st
( y in the carrier of Y & S1[a,y] )
then reconsider xa = x9 . a, ya = y9 . a as Element of Y by FUNCT_2:5;
take y = xa "\/" ya; :: thesis: ( y in the carrier of Y & S1[a,y] )
thus y in the carrier of Y ; :: thesis: S1[a,y]
take xa ; :: thesis: ex ya being Element of Y st
( xa = x9 . a & ya = y9 . a & y = xa "\/" ya )
take ya ; :: thesis: ( xa = x9 . a & ya = y9 . a & y = xa "\/" ya )
thus ( xa = x9 . a & ya = y9 . a & y = xa "\/" ya ) ; :: thesis: verum
end;
consider f being Function of X, the carrier of Y such that
A2: for a being object st a in X holds
S1[a,f . a] from FUNCT_2:sch 1(A1);
 f in Funcs (X, the carrier of Y) by FUNCT_2:8;
then reconsider z = f as Element of (Y |^ X) by Th28;
take z ; :: thesis: ( x <= z & y <= z & ( for b1 being Element of the carrier of (Y |^ X) holds
( not x <= b1 or not y <= b1 or z <= b1 ) ) )
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 object 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 y9 ; :: thesis: ex g being Function st
( y9 = y1 & g = z1 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = g . i & xi <= yi ) ) )
take f ; :: thesis: ( y9 = y1 & f = z1 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi ) ) )
thus ( y9 = y1 & f = z1 ) ; :: thesis: for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi )
let i be object ; :: thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi ) )
assume i in X ; :: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi )
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
reconsider yi = f . i, xi = y9 . i as Element of R ;
take R ; :: thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi )
take xi ; :: thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi )
take yi ; :: thesis: ( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi )
( R = Y & ex xa, ya being Element of Y st
( xa = x9 . i & ya = y9 . i & f . i = xa "\/" ya ) ) by A2;
hence ( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi ) by YELLOW_0:22; :: thesis: verum
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: verum
end;
A5: for z9 being Element of (Y |^ X) st z9 >= x & z9 >= y holds
z9 >= z
proof
let z9 be Element of (Y |^ X); :: thesis: ( z9 >= x & z9 >= y implies z9 >= z )
assume that
A6: z9 >= x and
A7: z9 >= y ; :: thesis: z9 >= z
z9 >= z
proof
reconsider z2 = z9, 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 object 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 object 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 object 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: ex g being Function st
( K = z3 & g = z2 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = g . i & xi <= yi ) ) )
take J ; :: thesis: ( K = z3 & J = z2 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi ) ) )
thus ( K = z3 & J = z2 ) ; :: thesis: for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi )
let i be object ; :: thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi ) )
assume i in X ; :: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi )
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 ;
take R ; :: thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi )
take xi ; :: thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi )
take yi ; :: thesis: ( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi )
A13: ( R = Y & ex xa, ya being Element of Y st
( xa = x9 . i & ya = y9 . i & f . i = xa "\/" ya ) ) by A2;
( 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: verum
end;
z3 in the carrier of (product (X --> Y)) ;
then z3 in product (Carrier (X --> Y)) by Def4;
hence z9 >= z by A12, Def4; :: thesis: verum
end;
hence z9 >= z ; :: thesis: verum
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 object 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 x9 ; :: thesis: ex g being Function st
( x9 = x1 & g = z1 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = g . i & xi <= yi ) ) )
take f ; :: thesis: ( x9 = x1 & f = z1 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi ) ) )
thus ( x9 = x1 & f = z1 ) ; :: thesis: for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi )
let i be object ; :: thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi ) )
assume i in X ; :: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi )
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
reconsider yi = f . i, xi = x9 . i as Element of R ;
take R ; :: thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi )
take xi ; :: thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi )
take yi ; :: thesis: ( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi )
( R = Y & ex xa, ya being Element of Y st
( xa = x9 . i & ya = y9 . i & f . i = xa "\/" ya ) ) by A2;
hence ( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi ) by YELLOW_0:22; :: thesis: verum
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: verum
end;
hence ( x <= z & y <= z & ( for b1 being Element of the carrier of (Y |^ X) holds
( not x <= b1 or not y <= b1 or z <= b1 ) ) ) by A3, A5; :: thesis: verum