defpred S₁[ 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:
reconsider At = A, Bt = B as non empty compact Subset of R^1 by JORDAN5A:25, TOPMETR:17;
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;

let x be Element of AB; :: thesis:
x in the carrier of AB ;
then x in [:A,B:] by A2, A1, BORSUK_1:def 2;
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:
thus S₁[x,t] by A6; :: thesis:

end;

consider f being RealMap of AB such that
A7: for x being Element of AB holds S₁[x,f . x] from FUNCT_2:sch 3(A3);
for Y being Subset of REAL st Y is open holds
f " Y is open

let Y be Subset of REAL; :: thesis:
assume A8: Y is open ; :: thesis:
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 )

let x be Point of AB; :: thesis:
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:
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 A8, RCOMP_1:18;
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 A1, XBOOLE_1:17;
reconsider YS = S /\ A as Subset of (R^1 | At) by A2, XBOOLE_1:17;
A14: s in T by A12, TOPREAL6:15, XREAL_1:215;
take YS ; :: thesis:
take YT ; :: thesis:
A15: T is open by JORDAN6:35;
S is open by JORDAN6:35;
hence ( YS is open & YT is open ) by A2, A1, A15, TSP_1:def 1; :: thesis:
A16: r in S by A12, TOPREAL6:15, XREAL_1:215;
x in the carrier of AB ;
then A17: x in [:A,B:] by A2, A1, BORSUK_1:def 2;
then s in B by A9, ZFMISC_1:87;
then A18: s in YT by A14, XBOOLE_0:def 4;
f .: [:YS,YT:] c= N

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in f .: [:YS,YT:] ; :: thesis:
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 A19, A21, ZFMISC_1:87;
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 A19, A21, ZFMISC_1:87;
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 A25, A24, XREAL_1:8;
then |.(|.(r1 - s1).| - |.(r - s).|).| < g by A23, XXREAL_0:2;
hence e in N by A13, A10, A20, A22, RCOMP_1:1; :: thesis:

end;

end;

hence f " Y is open by Th4; :: thesis:

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 A2, A1, A27, BORSUK_1:def 2;
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 ) }

let x be object ; :: thesis:
assume x in f .: the carrier of AB ; :: thesis:
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 A2, A1, A34, A36, BORSUK_1:def 2;
then A39: s1 in B by ZFMISC_1:87;
r1 in A by A38, ZFMISC_1:87;
hence x in { |.(r - s).| where r, s is Real : ( r in A & s in B ) } by A35, A37, A39; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { |.(r - s).| where r, s is Real : ( r in A & s in B ) } ; :: thesis:
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 A41, A42, ZFMISC_1:87;
then reconsider y = [r,s] as Element of AB by A2, A1, BORSUK_1:def 2;
consider r1, s1 being Real such that
A43: y = [r1,s1] and
A44: f . y = |.(r1 - s1).| by A7;
A45: s1 = s by A43, XTUPLE_0:1;
r1 = r by A43, XTUPLE_0:1;
hence x in f .: the carrier of AB by A40, A44, A45, FUNCT_2:35; :: thesis:

end;

reconsider r1 = r1, s1 = s1 as Real by A30, A31;
take r1 ; :: thesis:
take s1 ; :: thesis:
thus ( r1 in A & s1 in B ) by A29, A32, ZFMISC_1:87; :: thesis:
consider r, s being Real such that
A46: x = [r,s] and
A47: f . x = |.(r - s).| by A7;
A48: s1 = s by A32, A46, XTUPLE_0:1;
r1 = r by A32, A46, XTUPLE_0:1;
hence dist (A,B) = |.(r1 - s1).| by A28, A33, A47, A48, Def1; :: thesis: