let n be Element of NAT ; :: thesis:
let A, B be non empty compact Subset of (TOP-REAL n); :: thesis:
let f be continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]; :: thesis:
let g be RealMap of (TOP-REAL n); :: thesis:
assume A1: for q being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . p,q) where p is Point of (TOP-REAL n) : p in A } & g . q = inf G ) ; :: thesis:
A2: [:A,B:] is compact by BORSUK_3:27;
then A3: f .: [:A,B:] is compact by Th2;
f .: [:A,B:] is bounded by A2, Th2, RCOMP_1:28;
then A4: f .: [:A,B:] is bounded_below ;
A5: g .: B c= f .: [:A,B:]

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in g .: B ; :: thesis:
then consider q being Point of (TOP-REAL n) such that
A6: q in B and
A7: u = g . q by FUNCT_2:116;
consider p being Point of (TOP-REAL n) such that
A8: p in A by SUBSET_1:10;
consider G being Subset of REAL such that
A9: G = { (f . p1,q) where p1 is Point of (TOP-REAL n) : p1 in A } and
A10: u = inf G by A1, A7;
A11: f . p,q in G by A8, A9;
G c= f .: [:A,B:]

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in G ; :: thesis:
then consider p1 being Point of (TOP-REAL n) such that
A12: u = f . p1,q and
A13: p1 in A by A9;
[p1,q] in [:A,B:] by A6, A13, ZFMISC_1:106;
hence u in f .: [:A,B:] by A12, FUNCT_2:43; :: thesis:

end;

hence u in f .: [:A,B:] by A3, A10, A11, Th3; :: thesis:

end;

then A14: g .: B is bounded_below by A4, XXREAL_2:44;
A15: for r being real number st r in f .: [:A,B:] holds
inf (g .: B) <= r

let r be real number ; :: thesis:
assume r in f .: [:A,B:] ; :: thesis:
then consider pq being Point of [:(TOP-REAL n),(TOP-REAL n):] such that
A16: pq in [:A,B:] and
A17: r = f . pq by FUNCT_2:116;
pq in the carrier of [:(TOP-REAL n),(TOP-REAL n):] ;
then pq in [:the carrier of (TOP-REAL n),the carrier of (TOP-REAL n):] by BORSUK_1:def 5;
then consider p, q being set such that
A18: ( p in the carrier of (TOP-REAL n) & q in the carrier of (TOP-REAL n) ) and
A19: pq = [p,q] by ZFMISC_1:103;
A20: p in A by A16, A19, ZFMISC_1:106;
reconsider p = p, q = q as Point of (TOP-REAL n) by A18;
consider G being Subset of REAL such that
A21: G = { (f . p1,q) where p1 is Point of (TOP-REAL n) : p1 in A } and
A22: g . q = inf G by A1;
A23: q in B by A16, A19, ZFMISC_1:106;
G c= f .: [:A,B:]

let u be set ; :: according to TARSKI:def 3 :: thesis:
assume u in G ; :: thesis:
then consider p1 being Point of (TOP-REAL n) such that
A24: u = f . p1,q and
A25: p1 in A by A21;
[p1,q] in [:A,B:] by A23, A25, ZFMISC_1:106;
hence u in f .: [:A,B:] by A24, FUNCT_2:43; :: thesis:

end;

then A26: G is bounded_below by A4, XXREAL_2:44;
r = f . p,q by A17, A19;
then r in G by A20, A21;
then A27: g . q <= r by A22, A26, SEQ_4:def 5;
g . q in g .: B by A23, FUNCT_2:43;
then inf (g .: B) <= g . q by A14, SEQ_4:def 5;
hence inf (g .: B) <= r by A27, XXREAL_0:2; :: thesis:

end;

for s being real number st 0 < s holds
ex r being real number st
( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s )

let s be real number ; :: thesis:
assume 0 < s ; :: thesis:
then consider r being real number such that
A28: r in g .: B and
A29: r < (lower_bound (g .: B)) + s by A14, SEQ_4:def 5;
take r ; :: thesis:
thus r in f .: [:A,B:] by A5, A28; :: thesis:
thus r < (lower_bound (g .: B)) + s by A29; :: thesis:

end;

hence inf (f .: [:A,B:]) = inf (g .: B) by A4, A15, SEQ_4:def 5; :: thesis: