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 TOPMETR:24, TOPREAL6:81;
A1: ( the carrier of (R^1 | At) = At & the carrier of (R^1 | Bt) = Bt ) by PRE_TOPC:29;
reconsider AB = [:(R^1 | At),(R^1 | Bt):] as non empty compact TopSpace ;
defpred S₁[ set , set ] means ex r, s being Real st
( $1 = [r,s] & $2 = abs (r - s) );

A2: now

let x be Element of the carrier of AB; :: thesis:
x in the carrier of AB ;
then x in [:A,B:] by A1, BORSUK_1:def 5;
then consider r, s being set such that
A3: ( r in REAL & s in REAL ) and
A4: x = [r,s] by ZFMISC_1:103;
reconsider r = r, s = s as Real by A3;
take t = abs (r - s); :: thesis:
thus S₁[x,t] by A4; :: thesis:

end;

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

proof

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

proof

let x be Point of AB; :: thesis:
assume x in f " Y ; :: thesis:
then f . x in Y by FUNCT_1:def 13;
then consider N being Neighbourhood of f . x such that
A7: N c= Y by A6, RCOMP_1:39;
consider g being real number such that
A8: 0 < g and
A9: N = ].((f . x) - g),((f . x) + g).[ by RCOMP_1:def 7;
consider r, s being Real such that
A10: x = [r,s] and
A11: f . x = abs (r - s) by A5;
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:24;
reconsider YS = S /\ A as Subset of (R^1 | At) by A1, XBOOLE_1:17;
reconsider YT = T /\ B as Subset of (R^1 | Bt) by A1, XBOOLE_1:17;
take YS ; :: thesis:
take YT ; :: thesis:
( S is open & T is open ) by JORDAN6:46;
hence ( YS is open & YT is open ) by A1, TSP_1:def 1; :: thesis:
0 < g / 2 by A8, XREAL_1:217;
then A12: ( r in S & s in T ) by TOPREAL6:20;
x in the carrier of AB ;
then x in [:A,B:] by A1, BORSUK_1:def 5;
then ( r in A & s in B ) by A10, ZFMISC_1:106;
then ( r in YS & s in YT ) by A12, XBOOLE_0:def 4;
hence x in [:YS,YT:] by A10, ZFMISC_1:106; :: thesis:
A13: dom f = the carrier of AB by FUNCT_2:def 1;
f .: [:YS,YT:] c= N

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume e in f .: [:YS,YT:] ; :: thesis:
then consider y being Element of AB such that
A14: y in [:YS,YT:] and
A15: e = f . y by FUNCT_2:116;
consider r1, s1 being Real such that
A16: y = [r1,s1] and
A17: f . y = abs (r1 - s1) by A5;
r1 in YS by A14, A16, ZFMISC_1:106;
then r1 in ].(r - (g / 2)),(r + (g / 2)).[ by XBOOLE_0:def 4;
then A18: abs (r1 - r) < g / 2 by RCOMP_1:8;
s1 in YT by A14, A16, ZFMISC_1:106;
then s1 in ].(s - (g / 2)),(s + (g / 2)).[ by XBOOLE_0:def 4;
then A19: abs (s1 - s) < g / 2 by RCOMP_1:8;
g = (g / 2) + (g / 2) ;
then A20: (abs (r1 - r)) + (abs (s1 - s)) < g by A18, A19, XREAL_1:10;
abs ((abs (r1 - s1)) - (abs (r - s))) <= (abs (r1 - r)) + (abs (s1 - s)) by Th11;
then abs ((abs (r1 - s1)) - (abs (r - s))) < g by A20, XXREAL_0:2;
hence e in N by A9, A11, A15, A17, RCOMP_1:8; :: thesis:

end;

then f .: [:YS,YT:] c= Y by A7, XBOOLE_1:1;
hence [:YS,YT:] c= f " Y by A13, FUNCT_1:163; :: thesis:

end;

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

end;

then reconsider f = f as continuous RealMap of AB by PSCOMP_1:54;
f .: the carrier of AB is with_min by PSCOMP_1:def 15;
then inf (f .: the carrier of AB) in f .: the carrier of AB by PSCOMP_1:def 4;
then consider x being Element of AB such that
A21: x in the carrier of AB and
A22: inf (f .: the carrier of AB) = f . x by FUNCT_2:116;
A23: x in [:A,B:] by A1, A21, BORSUK_1:def 5;
then consider r1, s1 being set such that
A24: ( r1 in REAL & s1 in REAL ) and
A25: x = [r1,s1] by ZFMISC_1:103;
( r1 is Real & s1 is Real ) by A24;
then reconsider r1 = r1, s1 = s1 as real number ;
take r1 ; :: thesis:
take s1 ; :: thesis:
thus ( r1 in A & s1 in B ) by A23, A25, ZFMISC_1:106; :: thesis:
A26: f .: the carrier of AB = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) }

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:

let x be set ; :: thesis:
assume x in f .: the carrier of AB ; :: thesis:
then consider y being Element of AB such that
A27: y in the carrier of AB and
A28: x = f . y by FUNCT_2:116;
consider r1, s1 being Real such that
A29: y = [r1,s1] and
A30: f . y = abs (r1 - s1) by A5;
[r1,s1] in [:A,B:] by A1, A27, A29, BORSUK_1:def 5;
then ( r1 in A & s1 in B ) by ZFMISC_1:106;
hence x in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } by A28, A30; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ; :: thesis:
then consider r, s being Real such that
A31: x = abs (r - s) and
A32: ( r in A & s in B ) ;
[r,s] in [:A,B:] by A32, ZFMISC_1:106;
then reconsider y = [r,s] as Element of AB by A1, BORSUK_1:def 5;
consider r1, s1 being Real such that
A33: y = [r1,s1] and
A34: f . y = abs (r1 - s1) by A5;
( r1 = r & s1 = s ) by A33, ZFMISC_1:33;
hence x in f .: the carrier of AB by A31, A34, FUNCT_2:43; :: thesis:

end;

consider r, s being Real such that
A35: x = [r,s] and
A36: f . x = abs (r - s) by A5;
( r1 = r & s1 = s ) by A25, A35, ZFMISC_1:33;
hence dist A,B = abs (r1 - s1) by A22, A26, A36, Def2; :: thesis: