let n be Nat; :: thesis: for A, B being non empty compact Subset of ()
for f being continuous RealMap of [:(),():]
for g being RealMap of () st ( for q being Point of () ex G being Subset of REAL st
( G = { (f . (p,q)) where p is Point of () : p in A } & g . q = lower_bound G ) ) holds
lower_bound (f .: [:A,B:]) = lower_bound (g .: B)

let A, B be non empty compact Subset of (); :: thesis: for f being continuous RealMap of [:(),():]
for g being RealMap of () st ( for q being Point of () ex G being Subset of REAL st
( G = { (f . (p,q)) where p is Point of () : p in A } & g . q = lower_bound G ) ) holds
lower_bound (f .: [:A,B:]) = lower_bound (g .: B)

let f be continuous RealMap of [:(),():]; :: thesis: for g being RealMap of () st ( for q being Point of () ex G being Subset of REAL st
( G = { (f . (p,q)) where p is Point of () : p in A } & g . q = lower_bound G ) ) holds
lower_bound (f .: [:A,B:]) = lower_bound (g .: B)

let g be RealMap of (); :: thesis: ( ( for q being Point of () ex G being Subset of REAL st
( G = { (f . (p,q)) where p is Point of () : p in A } & g . q = lower_bound G ) ) implies lower_bound (f .: [:A,B:]) = lower_bound (g .: B) )

assume A1: for q being Point of () ex G being Subset of REAL st
( G = { (f . (p,q)) where p is Point of () : p in A } & g . q = lower_bound G ) ; :: thesis: lower_bound (f .: [:A,B:]) = lower_bound (g .: B)
A2: [:A,B:] is compact by BORSUK_3:23;
then A3: f .: [:A,B:] is compact by Th1;
A4: f .: [:A,B:] is real-bounded by ;
A5: g .: B c= f .: [:A,B:]
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in g .: B or u in f .: [:A,B:] )
assume u in g .: B ; :: thesis: u in f .: [:A,B:]
then consider q being Point of () such that
A6: q in B and
A7: u = g . q by FUNCT_2:65;
consider p being Point of () such that
A8: p in A by SUBSET_1:4;
consider G being Subset of REAL such that
A9: G = { (f . (p1,q)) where p1 is Point of () : p1 in A } and
A10: u = lower_bound G by A1, A7;
A11: f . (p,q) in G by A8, A9;
G c= f .: [:A,B:]
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in G or u in f .: [:A,B:] )
assume u in G ; :: thesis: u in f .: [:A,B:]
then consider p1 being Point of () such that
A12: u = f . (p1,q) and
A13: p1 in A by A9;
[p1,q] in [:A,B:] by ;
hence u in f .: [:A,B:] by ; :: thesis: verum
end;
hence u in f .: [:A,B:] by A3, A10, A11, Th2; :: thesis: verum
end;
then A14: g .: B is bounded_below by ;
A15: for r being Real st r in f .: [:A,B:] holds
lower_bound (g .: B) <= r
proof
let r be Real; :: thesis: ( r in f .: [:A,B:] implies lower_bound (g .: B) <= r )
assume r in f .: [:A,B:] ; :: thesis: lower_bound (g .: B) <= r
then consider pq being Point of [:(),():] such that
A16: pq in [:A,B:] and
A17: r = f . pq by FUNCT_2:65;
pq in the carrier of [:(),():] ;
then pq in [: the carrier of (), the carrier of ():] by BORSUK_1:def 2;
then consider p, q being object such that
A18: p in the carrier of () and
A19: q in the carrier of () and
A20: pq = [p,q] by ZFMISC_1:84;
A21: p in A by ;
reconsider p = p, q = q as Point of () by ;
consider G being Subset of REAL such that
A22: G = { (f . (p1,q)) where p1 is Point of () : p1 in A } and
A23: g . q = lower_bound G by A1;
A24: q in B by ;
G c= f .: [:A,B:]
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in G or u in f .: [:A,B:] )
assume u in G ; :: thesis: u in f .: [:A,B:]
then consider p1 being Point of () such that
A25: u = f . (p1,q) and
A26: p1 in A by A22;
[p1,q] in [:A,B:] by ;
hence u in f .: [:A,B:] by ; :: thesis: verum
end;
then A27: G is bounded_below by ;
r = f . (p,q) by ;
then r in G by ;
then A28: g . q <= r by ;
g . q in g .: B by ;
then lower_bound (g .: B) <= g . q by ;
hence lower_bound (g .: B) <= r by ; :: thesis: verum
end;
for s being Real st 0 < s holds
ex r being Real st
( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s )
proof
let s be Real; :: thesis: ( 0 < s implies ex r being Real st
( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s ) )

assume 0 < s ; :: thesis: ex r being Real st
( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s )

then consider r being Real such that
A29: r in g .: B and
A30: r < (lower_bound (g .: B)) + s by ;
take r ; :: thesis: ( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s )
thus r in f .: [:A,B:] by ; :: thesis: r < (lower_bound (g .: B)) + s
thus r < (lower_bound (g .: B)) + s by A30; :: thesis: verum
end;
hence lower_bound (f .: [:A,B:]) = lower_bound (g .: B) by ; :: thesis: verum