defpred S_{1}[ 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 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;

A7: for x being Element of AB holds S_{1}[x,f . x]
from FUNCT_2:sch 3(A3);

for Y being Subset of REAL st Y is open holds

f " Y is open

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 ) }

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 A29, A32, ZFMISC_1:87; :: 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 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: verum

( $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 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;

A3: now :: thesis: for x being Element of AB ex t being Element of REAL st S_{1}[x,t]

consider f being RealMap of AB such that let x be Element of AB; :: thesis: ex t being Element of REAL st S_{1}[x,t]

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: S_{1}[x,t]

thus S_{1}[x,t]
by A6; :: thesis: verum

end;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: S

thus S

A7: for x being Element of AB holds S

for Y being Subset of REAL st Y is open holds

f " Y is open

proof

then reconsider f = f as continuous RealMap of AB by PSCOMP_1:8;
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 )

end;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

hence
f " Y is open
by Th4; :: thesis: verum
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 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: 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 A2, A1, A15, TSP_1:def 1; :: thesis: ( x in [:YS,YT:] & [:YS,YT:] c= f " Y )

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

r in A by A9, A17, ZFMISC_1:87;

then r in YS by A16, XBOOLE_0:def 4;

hence x in [:YS,YT:] by A9, A18, ZFMISC_1:87; :: thesis: [:YS,YT:] c= f " Y

dom f = the carrier of AB by FUNCT_2:def 1;

hence [:YS,YT:] c= f " Y by A26, FUNCT_1:93; :: thesis: verum

end;( 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 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: 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 A2, A1, A15, TSP_1:def 1; :: thesis: ( x in [:YS,YT:] & [:YS,YT:] c= f " Y )

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

proof

then A26:
f .: [:YS,YT:] c= Y
by A11;
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 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: verum

end;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 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: verum

r in A by A9, A17, ZFMISC_1:87;

then r in YS by A16, XBOOLE_0:def 4;

hence x in [:YS,YT:] by A9, A18, ZFMISC_1:87; :: thesis: [:YS,YT:] c= f " Y

dom f = the carrier of AB by FUNCT_2:def 1;

hence [:YS,YT:] c= f " Y by A26, FUNCT_1:93; :: thesis: verum

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 ) }

proof

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 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: verum

end;

reconsider r1 = r1, s1 = s1 as Real by A30, A31;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 ; :: 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 )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 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: verum

end;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 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: verum

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 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: verum

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 A29, A32, ZFMISC_1:87; :: 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 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: verum