defpred S1[ set , set ] means ex r, s being Real st
( \$1 = [r,s] & \$2 = |.(r - s).| );
let A, B be non empty compact Subset of REAL; :: thesis: ex r, s being Real st
( r in A & s in B & dist (A,B) = |.(r - s).| )

reconsider At = A, Bt = B as non empty compact Subset of R^1 by ;
A1: the carrier of (R^1 | Bt) = Bt by PRE_TOPC:8;
reconsider AB = [:(R^1 | At),(R^1 | Bt):] as non empty compact TopSpace ;
A2: the carrier of (R^1 | At) = At by PRE_TOPC:8;
A3: now :: thesis: for x being Element of AB ex t being Element of REAL st S1[x,t]
let x be Element of AB; :: thesis: ex t being Element of REAL st S1[x,t]
x in the carrier of AB ;
then x in [:A,B:] by ;
then consider r, s being object such that
A4: r in REAL and
A5: s in REAL and
A6: x = [r,s] by ZFMISC_1:84;
reconsider r = r, s = s as Real by A4, A5;
reconsider t = |.(r - s).| as Element of REAL by XREAL_0:def 1;
take t = t; :: thesis: S1[x,t]
thus S1[x,t] by A6; :: thesis: verum
end;
consider f being RealMap of AB such that
A7: for x being Element of AB holds S1[x,f . x] from for Y being Subset of REAL st Y is open holds
f " Y is open
proof
let Y be Subset of REAL; :: thesis: ( Y is open implies f " Y is open )
assume A8: Y is open ; :: thesis: f " Y is open
for x being Point of AB st x in f " Y holds
ex YS being Subset of (R^1 | At) ex YT being Subset of (R^1 | Bt) st
( YS is open & YT is open & x in [:YS,YT:] & [:YS,YT:] c= f " Y )
proof
let x be Point of AB; :: thesis: ( x in f " Y implies ex YS being Subset of (R^1 | At) ex YT being Subset of (R^1 | Bt) st
( YS is open & YT is open & x in [:YS,YT:] & [:YS,YT:] c= f " Y ) )

consider r, s being Real such that
A9: x = [r,s] and
A10: f . x = |.(r - s).| by A7;
assume x in f " Y ; :: thesis: ex YS being Subset of (R^1 | At) ex YT being Subset of (R^1 | Bt) st
( YS is open & YT is open & x in [:YS,YT:] & [:YS,YT:] c= f " Y )

then f . x in Y by FUNCT_1:def 7;
then consider N being Neighbourhood of f . x such that
A11: N c= Y by ;
consider g being Real such that
A12: 0 < g and
A13: N = ].((f . x) - g),((f . x) + g).[ by RCOMP_1:def 6;
reconsider a = r - (g / 2), b = r + (g / 2), c = s - (g / 2), d = s + (g / 2) as Real ;
reconsider S = ].a,b.[, T = ].c,d.[ as Subset of R^1 by TOPMETR:17;
reconsider YT = T /\ B as Subset of (R^1 | Bt) by ;
reconsider YS = S /\ A as Subset of (R^1 | At) by ;
A14: s in T by ;
take YS ; :: thesis: ex YT being Subset of (R^1 | Bt) st
( YS is open & YT is open & x in [:YS,YT:] & [:YS,YT:] c= f " Y )

take YT ; :: thesis: ( YS is open & YT is open & x in [:YS,YT:] & [:YS,YT:] c= f " Y )
A15: T is open by JORDAN6:35;
S is open by JORDAN6:35;
hence ( YS is open & YT is open ) by ; :: thesis: ( x in [:YS,YT:] & [:YS,YT:] c= f " Y )
A16: r in S by ;
x in the carrier of AB ;
then A17: x in [:A,B:] by ;
then s in B by ;
then A18: s in YT by ;
f .: [:YS,YT:] c= N
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in f .: [:YS,YT:] or e in N )
assume e in f .: [:YS,YT:] ; :: thesis: e in N
then consider y being Element of AB such that
A19: y in [:YS,YT:] and
A20: e = f . y by FUNCT_2:65;
consider r1, s1 being Real such that
A21: y = [r1,s1] and
A22: f . y = |.(r1 - s1).| by A7;
A23: |.(|.(r1 - s1).| - |.(r - s).|).| <= |.(r1 - r).| + |.(s1 - s).| by Th2;
s1 in YT by ;
then s1 in ].(s - (g / 2)),(s + (g / 2)).[ by XBOOLE_0:def 4;
then A24: |.(s1 - s).| < g / 2 by RCOMP_1:1;
r1 in YS by ;
then r1 in ].(r - (g / 2)),(r + (g / 2)).[ by XBOOLE_0:def 4;
then A25: |.(r1 - r).| < g / 2 by RCOMP_1:1;
g = (g / 2) + (g / 2) ;
then |.(r1 - r).| + |.(s1 - s).| < g by ;
then |.(|.(r1 - s1).| - |.(r - s).|).| < g by ;
hence e in N by ; :: thesis: verum
end;
then A26: f .: [:YS,YT:] c= Y by A11;
r in A by ;
then r in YS by ;
hence x in [:YS,YT:] by ; :: thesis: [:YS,YT:] c= f " Y
dom f = the carrier of AB by FUNCT_2:def 1;
hence [:YS,YT:] c= f " Y by ; :: thesis: verum
end;
hence f " Y is open by Th4; :: thesis: verum
end;
then reconsider f = f as continuous RealMap of AB by PSCOMP_1:8;
f .: the carrier of AB is with_min by MEASURE6:def 13;
then lower_bound (f .: the carrier of AB) in f .: the carrier of AB by MEASURE6:def 5;
then consider x being Element of AB such that
A27: x in the carrier of AB and
A28: lower_bound (f .: the carrier of AB) = f . x by FUNCT_2:65;
A29: x in [:A,B:] by ;
then consider r1, s1 being object such that
A30: r1 in REAL and
A31: s1 in REAL and
A32: x = [r1,s1] by ZFMISC_1:84;
A33: f .: the carrier of AB = { |.(r - s).| where r, s is Real : ( r in A & s in B ) }
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { |.(r - s).| where r, s is Real : ( r in A & s in B ) } c= f .: the carrier of AB
let x be object ; :: thesis: ( x in f .: the carrier of AB implies x in { |.(r - s).| where r, s is Real : ( r in A & s in B ) } )
assume x in f .: the carrier of AB ; :: thesis: x in { |.(r - s).| where r, s is Real : ( r in A & s in B ) }
then consider y being Element of AB such that
A34: y in the carrier of AB and
A35: x = f . y by FUNCT_2:65;
consider r1, s1 being Real such that
A36: y = [r1,s1] and
A37: f . y = |.(r1 - s1).| by A7;
A38: [r1,s1] in [:A,B:] by ;
then A39: s1 in B by ZFMISC_1:87;
r1 in A by ;
hence x in { |.(r - s).| where r, s is Real : ( r in A & s in B ) } by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { |.(r - s).| where r, s is Real : ( r in A & s in B ) } or x in f .: the carrier of AB )
assume x in { |.(r - s).| where r, s is Real : ( r in A & s in B ) } ; :: thesis: x in f .: the carrier of AB
then consider r, s being Real such that
A40: x = |.(r - s).| and
A41: r in A and
A42: s in B ;
[r,s] in [:A,B:] by ;
then reconsider y = [r,s] as Element of AB by ;
consider r1, s1 being Real such that
A43: y = [r1,s1] and
A44: f . y = |.(r1 - s1).| by A7;
A45: s1 = s by ;
r1 = r by ;
hence x in f .: the carrier of AB by ; :: thesis: verum
end;
reconsider r1 = r1, s1 = s1 as Real by ;
take r1 ; :: thesis: ex s being Real st
( r1 in A & s in B & dist (A,B) = |.(r1 - s).| )

take s1 ; :: thesis: ( r1 in A & s1 in B & dist (A,B) = |.(r1 - s1).| )
thus ( r1 in A & s1 in B ) by ; :: thesis: dist (A,B) = |.(r1 - s1).|
consider r, s being Real such that
A46: x = [r,s] and
A47: f . x = |.(r - s).| by A7;
A48: s1 = s by ;
r1 = r by ;
hence dist (A,B) = |.(r1 - s1).| by A28, A33, A47, A48, Def1; :: thesis: verum