:: JCT_MISC semantic presentation begin scheme :: JCT_MISC:sch 1 NonEmpty{ F1() -> non empty set , F2( set ) -> set } : not { F2(a) where a is Element of F1() : verum } is empty proof consider a0 being set such that A1: a0 in F1() by XBOOLE_0:def_1; F2(a0) in { F2(a) where a is Element of F1() : verum } by A1; hence not { F2(a) where a is Element of F1() : verum } is empty ; ::_thesis: verum end; theorem Th1: :: JCT_MISC:1 for r, s, a, b being real number st r in [.a,b.] & s in [.a,b.] holds (r + s) / 2 in [.a,b.] proof let r, s be real number ; ::_thesis: for a, b being real number st r in [.a,b.] & s in [.a,b.] holds (r + s) / 2 in [.a,b.] let a, b be real number ; ::_thesis: ( r in [.a,b.] & s in [.a,b.] implies (r + s) / 2 in [.a,b.] ) assume that A1: r in [.a,b.] and A2: s in [.a,b.] ; ::_thesis: (r + s) / 2 in [.a,b.] reconsider a = a, b = b, r = r, s = s as Real by XREAL_0:def_1; A3: s <= b by A2, XXREAL_1:1; r <= b by A1, XXREAL_1:1; then r + s <= b + b by A3, XREAL_1:7; then A4: (r + s) / 2 <= (b + b) / 2 by XREAL_1:72; A5: a <= s by A2, XXREAL_1:1; a <= r by A1, XXREAL_1:1; then a + a <= r + s by A5, XREAL_1:7; then (a + a) / 2 <= (r + s) / 2 by XREAL_1:72; hence (r + s) / 2 in [.a,b.] by A4; ::_thesis: verum end; theorem Th2: :: JCT_MISC:2 for r0, s0, r, s being real number holds abs ((abs (r0 - s0)) - (abs (r - s))) <= (abs (r0 - r)) + (abs (s0 - s)) proof let r0, s0, r, s be real number ; ::_thesis: abs ((abs (r0 - s0)) - (abs (r - s))) <= (abs (r0 - r)) + (abs (s0 - s)) (r0 - s0) - (r - s) = (r0 - r) - (s0 - s) ; then A1: abs ((r0 - s0) - (r - s)) <= (abs (r0 - r)) + (abs (s0 - s)) by COMPLEX1:57; abs ((abs (r0 - s0)) - (abs (r - s))) <= abs ((r0 - s0) - (r - s)) by COMPLEX1:64; hence abs ((abs (r0 - s0)) - (abs (r - s))) <= (abs (r0 - r)) + (abs (s0 - s)) by A1, XXREAL_0:2; ::_thesis: verum end; theorem Th3: :: JCT_MISC:3 for t, r, s being real number st t in ].r,s.[ holds abs t < max ((abs r),(abs s)) proof let t, r, s be real number ; ::_thesis: ( t in ].r,s.[ implies abs t < max ((abs r),(abs s)) ) assume A1: t in ].r,s.[ ; ::_thesis: abs t < max ((abs r),(abs s)) reconsider r = r, t = t, s = s as Real by XREAL_0:def_1; A2: r < t by A1, XXREAL_1:4; A3: t < s by A1, XXREAL_1:4; percases ( t >= 0 or t < 0 ) ; supposeA4: t >= 0 ; ::_thesis: abs t < max ((abs r),(abs s)) then t = abs t by ABSVALUE:def_1; then abs t < abs s by A3, A4, ABSVALUE:def_1; hence abs t < max ((abs r),(abs s)) by XXREAL_0:30; ::_thesis: verum end; supposeA5: t < 0 ; ::_thesis: abs t < max ((abs r),(abs s)) then A6: - t = abs t by ABSVALUE:def_1; - r = abs r by A2, A5, ABSVALUE:def_1; then abs t < abs r by A2, A6, XREAL_1:24; hence abs t < max ((abs r),(abs s)) by XXREAL_0:30; ::_thesis: verum end; end; end; scheme :: JCT_MISC:sch 2 DoubleChoice{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , P1[ set , set , set ] } : ex a being Function of F1(),F2() ex b being Function of F1(),F3() st for i being Element of F1() holds P1[i,a . i,b . i] provided A1: for i being Element of F1() ex ai being Element of F2() ex bi being Element of F3() st P1[i,ai,bi] proof defpred S1[ set , set ] means P1[$1,$2 `1 ,$2 `2 ]; A2: for e being Element of F1() ex u being Element of [:F2(),F3():] st S1[e,u] proof let e be Element of F1(); ::_thesis: ex u being Element of [:F2(),F3():] st S1[e,u] consider ai being Element of F2(), bi being Element of F3() such that A3: P1[e,ai,bi] by A1; take [ai,bi] ; ::_thesis: ( [ai,bi] is Element of [:F2(),F3():] & S1[e,[ai,bi]] ) thus [ai,bi] is Element of [:F2(),F3():] by ZFMISC_1:87; ::_thesis: S1[e,[ai,bi]] thus S1[e,[ai,bi]] by A3; ::_thesis: verum end; consider f being Function of F1(),[:F2(),F3():] such that A4: for e being Element of F1() holds S1[e,f . e] from FUNCT_2:sch_3(A2); take pr1 f ; ::_thesis: ex b being Function of F1(),F3() st for i being Element of F1() holds P1[i,(pr1 f) . i,b . i] take pr2 f ; ::_thesis: for i being Element of F1() holds P1[i,(pr1 f) . i,(pr2 f) . i] let i be Element of F1(); ::_thesis: P1[i,(pr1 f) . i,(pr2 f) . i] A5: (f . i) `2 = (pr2 f) . i by FUNCT_2:def_6; (f . i) `1 = (pr1 f) . i by FUNCT_2:def_5; hence P1[i,(pr1 f) . i,(pr2 f) . i] by A4, A5; ::_thesis: verum end; theorem Th4: :: JCT_MISC:4 for S, T being non empty TopSpace for G being Subset of [:S,T:] st ( for x being Point of [:S,T:] st x in G holds ex GS being Subset of S ex GT being Subset of T st ( GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G ) ) holds G is open proof let S, T be non empty TopSpace; ::_thesis: for G being Subset of [:S,T:] st ( for x being Point of [:S,T:] st x in G holds ex GS being Subset of S ex GT being Subset of T st ( GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G ) ) holds G is open let G be Subset of [:S,T:]; ::_thesis: ( ( for x being Point of [:S,T:] st x in G holds ex GS being Subset of S ex GT being Subset of T st ( GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G ) ) implies G is open ) assume A1: for x being Point of [:S,T:] st x in G holds ex GS being Subset of S ex GT being Subset of T st ( GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G ) ; ::_thesis: G is open set A = { [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) } ; { [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) } c= bool the carrier of [:S,T:] proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) } or e in bool the carrier of [:S,T:] ) assume e in { [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) } ; ::_thesis: e in bool the carrier of [:S,T:] then ex GS being Subset of S ex GT being Subset of T st ( e = [:GS,GT:] & GS is open & GT is open & [:GS,GT:] c= G ) ; hence e in bool the carrier of [:S,T:] ; ::_thesis: verum end; then reconsider A = { [:GS,GT:] where GS is Subset of S, GT is Subset of T : ( GS is open & GT is open & [:GS,GT:] c= G ) } as Subset-Family of [:S,T:] ; reconsider A = A as Subset-Family of [:S,T:] ; for x being set holds ( x in G iff ex Y being set st ( x in Y & Y in A ) ) proof let x be set ; ::_thesis: ( x in G iff ex Y being set st ( x in Y & Y in A ) ) thus ( x in G implies ex Y being set st ( x in Y & Y in A ) ) ::_thesis: ( ex Y being set st ( x in Y & Y in A ) implies x in G ) proof assume x in G ; ::_thesis: ex Y being set st ( x in Y & Y in A ) then consider GS being Subset of S, GT being Subset of T such that A2: GS is open and A3: GT is open and A4: x in [:GS,GT:] and A5: [:GS,GT:] c= G by A1; take [:GS,GT:] ; ::_thesis: ( x in [:GS,GT:] & [:GS,GT:] in A ) thus ( x in [:GS,GT:] & [:GS,GT:] in A ) by A2, A3, A4, A5; ::_thesis: verum end; given Y being set such that A6: x in Y and A7: Y in A ; ::_thesis: x in G ex GS being Subset of S ex GT being Subset of T st ( Y = [:GS,GT:] & GS is open & GT is open & [:GS,GT:] c= G ) by A7; hence x in G by A6; ::_thesis: verum end; then A8: G = union A by TARSKI:def_4; for e being set st e in A holds ex X1 being Subset of S ex Y1 being Subset of T st ( e = [:X1,Y1:] & X1 is open & Y1 is open ) proof let e be set ; ::_thesis: ( e in A implies ex X1 being Subset of S ex Y1 being Subset of T st ( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) assume e in A ; ::_thesis: ex X1 being Subset of S ex Y1 being Subset of T st ( e = [:X1,Y1:] & X1 is open & Y1 is open ) then ex GS being Subset of S ex GT being Subset of T st ( e = [:GS,GT:] & GS is open & GT is open & [:GS,GT:] c= G ) ; hence ex X1 being Subset of S ex Y1 being Subset of T st ( e = [:X1,Y1:] & X1 is open & Y1 is open ) ; ::_thesis: verum end; hence G is open by A8, BORSUK_1:5; ::_thesis: verum end; begin theorem Th5: :: JCT_MISC:5 for A, B being compact Subset of REAL holds A /\ B is compact proof let A, B be compact Subset of REAL; ::_thesis: A /\ B is compact let s1 be Real_Sequence; :: according to RCOMP_1:def_3 ::_thesis: ( not proj2 s1 c= A /\ B or ex b1 being Element of bool [:NAT,REAL:] st ( b1 is subsequence of s1 & b1 is convergent & lim b1 in A /\ B ) ) assume A1: rng s1 c= A /\ B ; ::_thesis: ex b1 being Element of bool [:NAT,REAL:] st ( b1 is subsequence of s1 & b1 is convergent & lim b1 in A /\ B ) A2: A /\ B c= B by XBOOLE_1:17; A /\ B c= A by XBOOLE_1:17; then rng s1 c= A by A1, XBOOLE_1:1; then consider s2 being Real_Sequence such that A3: s2 is subsequence of s1 and A4: s2 is convergent and A5: lim s2 in A by RCOMP_1:def_3; rng s2 c= rng s1 by A3, VALUED_0:21; then rng s2 c= A /\ B by A1, XBOOLE_1:1; then rng s2 c= B by A2, XBOOLE_1:1; then consider s3 being Real_Sequence such that A6: s3 is subsequence of s2 and A7: s3 is convergent and A8: lim s3 in B by RCOMP_1:def_3; take s3 ; ::_thesis: ( s3 is subsequence of s1 & s3 is convergent & lim s3 in A /\ B ) thus s3 is subsequence of s1 by A3, A6, VALUED_0:20; ::_thesis: ( s3 is convergent & lim s3 in A /\ B ) thus s3 is convergent by A7; ::_thesis: lim s3 in A /\ B lim s3 = lim s2 by A4, A6, SEQ_4:17; hence lim s3 in A /\ B by A5, A8, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: JCT_MISC:6 for T being non empty TopSpace for f being continuous RealMap of T for A being Subset of T st A is connected holds f .: A is interval proof let T be non empty TopSpace; ::_thesis: for f being continuous RealMap of T for A being Subset of T st A is connected holds f .: A is interval let f be continuous RealMap of T; ::_thesis: for A being Subset of T st A is connected holds f .: A is interval let A be Subset of T; ::_thesis: ( A is connected implies f .: A is interval ) assume A1: A is connected ; ::_thesis: f .: A is interval let r, s be ext-real number ; :: according to XXREAL_2:def_12 ::_thesis: ( not r in f .: A or not s in f .: A or [.r,s.] c= f .: A ) A2: A c= f " (f .: A) by FUNCT_2:42; assume A3: r in f .: A ; ::_thesis: ( not s in f .: A or [.r,s.] c= f .: A ) then consider p being Point of T such that A4: p in A and A5: r = f . p by FUNCT_2:65; assume A6: s in f .: A ; ::_thesis: [.r,s.] c= f .: A then consider q being Point of T such that A7: q in A and A8: s = f . q by FUNCT_2:65; assume A9: not [.r,s.] c= f .: A ; ::_thesis: contradiction reconsider r = r, s = s as Real by A3, A6; consider t being Real such that A10: t in [.r,s.] and A11: not t in f .: A by A9, SUBSET_1:2; reconsider r = r, s = s, t = t as Real ; set P1 = f " (left_open_halfline t); set Q1 = f " (right_open_halfline t); set P = (f " (left_open_halfline t)) /\ A; set Q = (f " (right_open_halfline t)) /\ A; set X = (left_open_halfline t) \/ (right_open_halfline t); A12: f " (right_open_halfline t) is open by PSCOMP_1:8; t <= s by A10, XXREAL_1:1; then A13: t < s by A6, A11, XXREAL_0:1; right_open_halfline t = { r1 where r1 is Real : t < r1 } by XXREAL_1:230; then s in right_open_halfline t by A13; then q in f " (right_open_halfline t) by A8, FUNCT_2:38; then A14: (f " (right_open_halfline t)) /\ A <> {} T by A7, XBOOLE_0:def_4; (left_open_halfline t) /\ (right_open_halfline t) = ].t,t.[ by XXREAL_1:269 .= {} by XXREAL_1:28 ; then left_open_halfline t misses right_open_halfline t by XBOOLE_0:def_7; then f " (left_open_halfline t) misses f " (right_open_halfline t) by FUNCT_1:71; then (f " (left_open_halfline t)) /\ (f " (right_open_halfline t)) = {} by XBOOLE_0:def_7; then A15: (f " (left_open_halfline t)) /\ (f " (right_open_halfline t)) misses ((f " (left_open_halfline t)) /\ A) \/ ((f " (right_open_halfline t)) /\ A) by XBOOLE_1:65; reconsider Y = {t} as Subset of REAL ; Y ` = REAL \ [.t,t.] by XXREAL_1:17 .= (left_open_halfline t) \/ (right_open_halfline t) by XXREAL_1:385 ; then A16: (f " Y) ` = f " ((left_open_halfline t) \/ (right_open_halfline t)) by FUNCT_2:100 .= (f " (left_open_halfline t)) \/ (f " (right_open_halfline t)) by RELAT_1:140 ; f " {t} misses f " (f .: A) by A11, FUNCT_1:71, ZFMISC_1:50; then f " {t} misses A by A2, XBOOLE_1:63; then A c= (f " (left_open_halfline t)) \/ (f " (right_open_halfline t)) by A16, SUBSET_1:23; then A17: A = A /\ ((f " (left_open_halfline t)) \/ (f " (right_open_halfline t))) by XBOOLE_1:28 .= ((f " (left_open_halfline t)) /\ A) \/ ((f " (right_open_halfline t)) /\ A) by XBOOLE_1:23 ; A18: (f " (left_open_halfline t)) /\ A c= f " (left_open_halfline t) by XBOOLE_1:17; r <= t by A10, XXREAL_1:1; then A19: r < t by A3, A11, XXREAL_0:1; left_open_halfline t = { r1 where r1 is Real : r1 < t } by XXREAL_1:229; then r in left_open_halfline t by A19; then p in f " (left_open_halfline t) by A5, FUNCT_2:38; then A20: (f " (left_open_halfline t)) /\ A <> {} T by A4, XBOOLE_0:def_4; A21: (f " (right_open_halfline t)) /\ A c= f " (right_open_halfline t) by XBOOLE_1:17; f " (left_open_halfline t) is open by PSCOMP_1:8; then (f " (left_open_halfline t)) /\ A,(f " (right_open_halfline t)) /\ A are_separated by A12, A18, A21, A15, TSEP_1:45; hence contradiction by A1, A17, A20, A14, CONNSP_1:15; ::_thesis: verum end; definition let A, B be Subset of REAL; func dist (A,B) -> real number means :Def1: :: JCT_MISC:def 1 ex X being Subset of REAL st ( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & it = lower_bound X ); existence ex b1 being real number ex X being Subset of REAL st ( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & b1 = lower_bound X ) proof set Y = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ; { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } c= REAL proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } or e in REAL ) assume e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ; ::_thesis: e in REAL then ex r, s being Element of REAL st ( e = abs (r - s) & r in A & s in B ) ; hence e in REAL ; ::_thesis: verum end; then reconsider Y0 = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } as Subset of REAL ; take lower_bound Y0 ; ::_thesis: ex X being Subset of REAL st ( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & lower_bound Y0 = lower_bound X ) thus ex X being Subset of REAL st ( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & lower_bound Y0 = lower_bound X ) ; ::_thesis: verum end; uniqueness for b1, b2 being real number st ex X being Subset of REAL st ( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & b1 = lower_bound X ) & ex X being Subset of REAL st ( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & b2 = lower_bound X ) holds b1 = b2 ; commutativity for b1 being real number for A, B being Subset of REAL st ex X being Subset of REAL st ( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & b1 = lower_bound X ) holds ex X being Subset of REAL st ( X = { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } & b1 = lower_bound X ) proof let IT be real number ; ::_thesis: for A, B being Subset of REAL st ex X being Subset of REAL st ( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & IT = lower_bound X ) holds ex X being Subset of REAL st ( X = { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } & IT = lower_bound X ) let A, B be Subset of REAL; ::_thesis: ( ex X being Subset of REAL st ( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & IT = lower_bound X ) implies ex X being Subset of REAL st ( X = { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } & IT = lower_bound X ) ) given X0 being Subset of REAL such that A1: X0 = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } and A2: IT = lower_bound X0 ; ::_thesis: ex X being Subset of REAL st ( X = { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } & IT = lower_bound X ) set Y = { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } ; { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } c= REAL proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } or e in REAL ) assume e in { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } ; ::_thesis: e in REAL then ex r, s being Element of REAL st ( e = abs (r - s) & r in B & s in A ) ; hence e in REAL ; ::_thesis: verum end; then reconsider Y0 = { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } as Subset of REAL ; take Y0 ; ::_thesis: ( Y0 = { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } & IT = lower_bound Y0 ) thus Y0 = { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } ; ::_thesis: IT = lower_bound Y0 X0 = Y0 proof thus X0 c= Y0 :: according to XBOOLE_0:def_10 ::_thesis: Y0 c= X0 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X0 or x in Y0 ) assume x in X0 ; ::_thesis: x in Y0 then consider r, s being Element of REAL such that A3: x = abs (r - s) and A4: r in A and A5: s in B by A1; x = abs (s - r) by A3, UNIFORM1:11; hence x in Y0 by A4, A5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y0 or x in X0 ) assume x in Y0 ; ::_thesis: x in X0 then consider r, s being Element of REAL such that A6: x = abs (r - s) and A7: r in B and A8: s in A ; x = abs (s - r) by A6, UNIFORM1:11; hence x in X0 by A1, A7, A8; ::_thesis: verum end; hence IT = lower_bound Y0 by A2; ::_thesis: verum end; end; :: deftheorem Def1 defines dist JCT_MISC:def_1_:_ for A, B being Subset of REAL for b3 being real number holds ( b3 = dist (A,B) iff ex X being Subset of REAL st ( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & b3 = lower_bound X ) ); theorem Th7: :: JCT_MISC:7 for A, B being Subset of REAL for r, s being real number st r in A & s in B holds abs (r - s) >= dist (A,B) proof let A, B be Subset of REAL; ::_thesis: for r, s being real number st r in A & s in B holds abs (r - s) >= dist (A,B) set Y = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ; let r, s be real number ; ::_thesis: ( r in A & s in B implies abs (r - s) >= dist (A,B) ) assume that A1: r in A and A2: s in B ; ::_thesis: abs (r - s) >= dist (A,B) { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } c= REAL proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } or e in REAL ) assume e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ; ::_thesis: e in REAL then ex r, s being Real st ( e = abs (r - s) & r in A & s in B ) ; hence e in REAL ; ::_thesis: verum end; then reconsider Y0 = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } as Subset of REAL ; A3: Y0 is bounded_below proof take 0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of Y0 let r0 be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r0 in Y0 or 0 <= r0 ) assume r0 in Y0 ; ::_thesis: 0 <= r0 then ex r, s being Real st ( r0 = abs (r - s) & r in A & s in B ) ; hence 0 <= r0 by COMPLEX1:46; ::_thesis: verum end; A4: dist (A,B) = lower_bound Y0 by Def1; abs (r - s) in Y0 by A1, A2; hence abs (r - s) >= dist (A,B) by A4, A3, SEQ_4:def_2; ::_thesis: verum end; theorem Th8: :: JCT_MISC:8 for A, B being Subset of REAL for C, D being non empty Subset of REAL st C c= A & D c= B holds dist (A,B) <= dist (C,D) proof let A, B be Subset of REAL; ::_thesis: for C, D being non empty Subset of REAL st C c= A & D c= B holds dist (A,B) <= dist (C,D) let C, D be non empty Subset of REAL; ::_thesis: ( C c= A & D c= B implies dist (A,B) <= dist (C,D) ) assume that A1: C c= A and A2: D c= B ; ::_thesis: dist (A,B) <= dist (C,D) consider s0 being set such that A3: s0 in D by XBOOLE_0:def_1; set Y = { (abs (r - s)) where r, s is Element of REAL : ( r in C & s in D ) } ; consider r0 being set such that A4: r0 in C by XBOOLE_0:def_1; A5: { (abs (r - s)) where r, s is Element of REAL : ( r in C & s in D ) } c= REAL proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (abs (r - s)) where r, s is Element of REAL : ( r in C & s in D ) } or e in REAL ) assume e in { (abs (r - s)) where r, s is Element of REAL : ( r in C & s in D ) } ; ::_thesis: e in REAL then ex r, s being Real st ( e = abs (r - s) & r in C & s in D ) ; hence e in REAL ; ::_thesis: verum end; reconsider r0 = r0, s0 = s0 as real number by A4, A3; abs (r0 - s0) in { (abs (r - s)) where r, s is Element of REAL : ( r in C & s in D ) } by A4, A3; then reconsider Y = { (abs (r - s)) where r, s is Element of REAL : ( r in C & s in D ) } as non empty Subset of REAL by A5; set X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ; { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } c= REAL proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } or e in REAL ) assume e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ; ::_thesis: e in REAL then ex r, s being Real st ( e = abs (r - s) & r in A & s in B ) ; hence e in REAL ; ::_thesis: verum end; then reconsider X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } as Subset of REAL ; A6: Y c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in X ) assume x in Y ; ::_thesis: x in X then ex r, s being Real st ( x = abs (r - s) & r in C & s in D ) ; hence x in X by A1, A2; ::_thesis: verum end; A7: X is bounded_below proof take 0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of X let r0 be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r0 in X or 0 <= r0 ) assume r0 in X ; ::_thesis: 0 <= r0 then ex r, s being Real st ( r0 = abs (r - s) & r in A & s in B ) ; hence 0 <= r0 by COMPLEX1:46; ::_thesis: verum end; A8: dist (C,D) = lower_bound Y by Def1; dist (A,B) = lower_bound X by Def1; hence dist (A,B) <= dist (C,D) by A7, A8, A6, SEQ_4:47; ::_thesis: verum end; theorem Th9: :: JCT_MISC:9 for A, B being non empty compact Subset of REAL ex r, s being real number st ( r in A & s in B & dist (A,B) = abs (r - s) ) proof defpred S1[ set , set ] means ex r, s being Real st ( $1 = [r,s] & $2 = abs (r - s) ); let A, B be non empty compact Subset of REAL; ::_thesis: ex r, s being real number st ( r in A & s in B & dist (A,B) = abs (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_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 A2, A1, BORSUK_1:def_2; then consider r, s being set 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; take t = abs (r - s); ::_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 FUNCT_2:sch_3(A3); 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 = abs (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 number 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 let e be set ; :: 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 = abs (r1 - s1) by A7; A23: abs ((abs (r1 - s1)) - (abs (r - s))) <= (abs (r1 - r)) + (abs (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: abs (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: abs (r1 - r) < g / 2 by RCOMP_1:1; g = (g / 2) + (g / 2) ; then (abs (r1 - r)) + (abs (s1 - s)) < g by A25, A24, XREAL_1:8; then abs ((abs (r1 - s1)) - (abs (r - s))) < g by A23, XXREAL_0:2; hence e in N by A13, A10, A20, A22, RCOMP_1:1; ::_thesis: verum end; then A26: f .: [:YS,YT:] c= Y by A11, XBOOLE_1:1; 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; 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 A2, A1, A27, BORSUK_1:def_2; then consider r1, s1 being set 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 = { (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: { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } c= f .: the carrier of AB let x be set ; ::_thesis: ( x in f .: the carrier of AB implies x in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ) assume x in f .: the carrier of AB ; ::_thesis: x in { (abs (r - s)) where r, s is Element of 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 = abs (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 { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } by A35, A37, A39; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } or x in f .: the carrier of AB ) assume x in { (abs (r - s)) where r, s is Element of 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 = abs (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 = abs (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 number by A30, A31; take r1 ; ::_thesis: ex s being real number st ( r1 in A & s in B & dist (A,B) = abs (r1 - s) ) take s1 ; ::_thesis: ( r1 in A & s1 in B & dist (A,B) = abs (r1 - s1) ) thus ( r1 in A & s1 in B ) by A29, A32, ZFMISC_1:87; ::_thesis: dist (A,B) = abs (r1 - s1) consider r, s being Real such that A46: x = [r,s] and A47: f . x = abs (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) = abs (r1 - s1) by A28, A33, A47, A48, Def1; ::_thesis: verum end; theorem Th10: :: JCT_MISC:10 for A, B being non empty compact Subset of REAL holds dist (A,B) >= 0 proof let A, B be non empty compact Subset of REAL; ::_thesis: dist (A,B) >= 0 set X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ; consider r0 being set such that A1: r0 in A by XBOOLE_0:def_1; A2: { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } c= REAL proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } or e in REAL ) assume e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ; ::_thesis: e in REAL then ex r, s being Real st ( e = abs (r - s) & r in A & s in B ) ; hence e in REAL ; ::_thesis: verum end; consider s0 being set such that A3: s0 in B by XBOOLE_0:def_1; reconsider r0 = r0, s0 = s0 as real number by A1, A3; abs (r0 - s0) in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } by A1, A3; then reconsider X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } as non empty Subset of REAL by A2; A4: for t being real number st t in X holds t >= 0 proof let t be real number ; ::_thesis: ( t in X implies t >= 0 ) assume t in X ; ::_thesis: t >= 0 then ex r, s being Real st ( t = abs (r - s) & r in A & s in B ) ; hence t >= 0 by COMPLEX1:46; ::_thesis: verum end; dist (A,B) = lower_bound X by Def1; hence dist (A,B) >= 0 by A4, SEQ_4:43; ::_thesis: verum end; theorem Th11: :: JCT_MISC:11 for A, B being non empty compact Subset of REAL st A misses B holds dist (A,B) > 0 proof let A, B be non empty compact Subset of REAL; ::_thesis: ( A misses B implies dist (A,B) > 0 ) assume A1: A misses B ; ::_thesis: dist (A,B) > 0 consider r0, s0 being real number such that A2: r0 in A and A3: s0 in B and A4: dist (A,B) = abs (r0 - s0) by Th9; reconsider r0 = r0, s0 = s0 as Real by XREAL_0:def_1; assume dist (A,B) <= 0 ; ::_thesis: contradiction then abs (r0 - s0) = 0 by A4, Th10; then r0 = s0 by GOBOARD7:2; hence contradiction by A1, A2, A3, XBOOLE_0:3; ::_thesis: verum end; theorem :: JCT_MISC:12 for e, f being real number for A, B being compact Subset of REAL st A misses B & A c= [.e,f.] & B c= [.e,f.] holds for S being Function of NAT,(bool REAL) st ( for i being Element of NAT holds ( S . i is interval & S . i meets A & S . i meets B ) ) holds ex r being real number st ( r in [.e,f.] & not r in A \/ B & ( for i being Element of NAT ex k being Element of NAT st ( i <= k & r in S . k ) ) ) proof let e, f be real number ; ::_thesis: for A, B being compact Subset of REAL st A misses B & A c= [.e,f.] & B c= [.e,f.] holds for S being Function of NAT,(bool REAL) st ( for i being Element of NAT holds ( S . i is interval & S . i meets A & S . i meets B ) ) holds ex r being real number st ( r in [.e,f.] & not r in A \/ B & ( for i being Element of NAT ex k being Element of NAT st ( i <= k & r in S . k ) ) ) let A, B be compact Subset of REAL; ::_thesis: ( A misses B & A c= [.e,f.] & B c= [.e,f.] implies for S being Function of NAT,(bool REAL) st ( for i being Element of NAT holds ( S . i is interval & S . i meets A & S . i meets B ) ) holds ex r being real number st ( r in [.e,f.] & not r in A \/ B & ( for i being Element of NAT ex k being Element of NAT st ( i <= k & r in S . k ) ) ) ) assume that A1: A misses B and A2: A c= [.e,f.] and A3: B c= [.e,f.] ; ::_thesis: for S being Function of NAT,(bool REAL) st ( for i being Element of NAT holds ( S . i is interval & S . i meets A & S . i meets B ) ) holds ex r being real number st ( r in [.e,f.] & not r in A \/ B & ( for i being Element of NAT ex k being Element of NAT st ( i <= k & r in S . k ) ) ) let S be Function of NAT,(bool REAL); ::_thesis: ( ( for i being Element of NAT holds ( S . i is interval & S . i meets A & S . i meets B ) ) implies ex r being real number st ( r in [.e,f.] & not r in A \/ B & ( for i being Element of NAT ex k being Element of NAT st ( i <= k & r in S . k ) ) ) ) assume A4: for i being Element of NAT holds ( S . i is interval & S . i meets A & S . i meets B ) ; ::_thesis: ex r being real number st ( r in [.e,f.] & not r in A \/ B & ( for i being Element of NAT ex k being Element of NAT st ( i <= k & r in S . k ) ) ) defpred S1[ set , Subset of REAL] means ( not $2 is empty & $2 is closed_interval & $2 meets A & $2 meets B & $2 c= S . $1 ); A5: for i being Element of NAT ex u being Subset of REAL st S1[i,u] proof let i be Element of NAT ; ::_thesis: ex u being Subset of REAL st S1[i,u] A6: S . i is interval by A4; S . i meets B by A4; then consider y being set such that A7: y in S . i and A8: y in B by XBOOLE_0:3; S . i meets A by A4; then consider x being set such that A9: x in S . i and A10: x in A by XBOOLE_0:3; reconsider y = y as Real by A8; reconsider x = x as Real by A10; percases ( x <= y or y <= x ) ; supposeA11: x <= y ; ::_thesis: ex u being Subset of REAL st S1[i,u] take [.x,y.] ; ::_thesis: S1[i,[.x,y.]] thus ( not [.x,y.] is empty & [.x,y.] is closed_interval ) by A11, MEASURE5:14; ::_thesis: ( [.x,y.] meets A & [.x,y.] meets B & [.x,y.] c= S . i ) x in [.x,y.] by A11; hence [.x,y.] meets A by A10, XBOOLE_0:3; ::_thesis: ( [.x,y.] meets B & [.x,y.] c= S . i ) y in [.x,y.] by A11; hence [.x,y.] meets B by A8, XBOOLE_0:3; ::_thesis: [.x,y.] c= S . i thus [.x,y.] c= S . i by A9, A7, A6, XXREAL_2:def_12; ::_thesis: verum end; supposeA12: y <= x ; ::_thesis: ex u being Subset of REAL st S1[i,u] take [.y,x.] ; ::_thesis: S1[i,[.y,x.]] thus ( not [.y,x.] is empty & [.y,x.] is closed_interval ) by A12, MEASURE5:14; ::_thesis: ( [.y,x.] meets A & [.y,x.] meets B & [.y,x.] c= S . i ) x in [.y,x.] by A12; hence [.y,x.] meets A by A10, XBOOLE_0:3; ::_thesis: ( [.y,x.] meets B & [.y,x.] c= S . i ) y in [.y,x.] by A12; hence [.y,x.] meets B by A8, XBOOLE_0:3; ::_thesis: [.y,x.] c= S . i thus [.y,x.] c= S . i by A9, A7, A6, XXREAL_2:def_12; ::_thesis: verum end; end; end; consider T being Function of NAT,(bool REAL) such that A13: for i being Element of NAT holds S1[i,T . i] from FUNCT_2:sch_3(A5); T . 0 meets B by A13; then A14: not B is empty by XBOOLE_1:65; deffunc H1( Element of NAT ) -> Element of bool REAL = (T . $1) /\ B; deffunc H2( Element of NAT ) -> Element of bool REAL = (T . $1) /\ A; consider SA being Function of NAT,(bool REAL) such that A15: for i being Element of NAT holds SA . i = H2(i) from FUNCT_2:sch_4(); consider SB being Function of NAT,(bool REAL) such that A16: for i being Element of NAT holds SB . i = H1(i) from FUNCT_2:sch_4(); defpred S2[ Element of NAT , Real, Real] means ( $2 in SA . $1 & $3 in SB . $1 & dist ((SA . $1),(SB . $1)) = abs ($2 - $3) ); A17: for i being Element of NAT ex ai, bi being Real st S2[i,ai,bi] proof let i be Element of NAT ; ::_thesis: ex ai, bi being Real st S2[i,ai,bi] reconsider Si = T . i as non empty closed_interval Subset of REAL by A13; A18: T . i meets B by A13; A19: SA . i = Si /\ A by A15; A20: SB . i = Si /\ B by A16; T . i meets A by A13; then reconsider SAi = SA . i, SBi = SB . i as non empty compact Subset of REAL by A18, A19, A20, Th5, XBOOLE_0:def_7; consider ai, bi being real number such that A21: ai in SAi and A22: bi in SBi and A23: dist (SAi,SBi) = abs (ai - bi) by Th9; reconsider ai = ai, bi = bi as Real by XREAL_0:def_1; take ai ; ::_thesis: ex bi being Real st S2[i,ai,bi] take bi ; ::_thesis: S2[i,ai,bi] thus S2[i,ai,bi] by A21, A22, A23; ::_thesis: verum end; consider sa, sb being Real_Sequence such that A24: for i being Element of NAT holds S2[i,sa . i,sb . i] from JCT_MISC:sch_2(A17); rng sa c= [.e,f.] proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in rng sa or u in [.e,f.] ) assume u in rng sa ; ::_thesis: u in [.e,f.] then consider x being set such that A25: x in dom sa and A26: u = sa . x by FUNCT_1:def_3; reconsider n = x as Element of NAT by A25; sa . n in SA . n by A24; then u in (T . n) /\ A by A15, A26; then u in A by XBOOLE_0:def_4; hence u in [.e,f.] by A2; ::_thesis: verum end; then consider ga being Real_Sequence such that A27: ga is subsequence of sa and A28: ga is convergent and A29: lim ga in [.e,f.] by RCOMP_1:def_3; consider Nseq being increasing sequence of NAT such that A30: ga = sa * Nseq by A27, VALUED_0:def_17; set gb = sb * Nseq; rng (sb * Nseq) c= [.e,f.] proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in rng (sb * Nseq) or u in [.e,f.] ) assume u in rng (sb * Nseq) ; ::_thesis: u in [.e,f.] then consider x being set such that A31: x in dom (sb * Nseq) and A32: u = (sb * Nseq) . x by FUNCT_1:def_3; reconsider n = x as Element of NAT by A31; (sb * Nseq) . n = sb . (Nseq . n) by FUNCT_2:15; then (sb * Nseq) . n in SB . (Nseq . n) by A24; then u in (T . (Nseq . n)) /\ B by A16, A32; then u in B by XBOOLE_0:def_4; hence u in [.e,f.] by A3; ::_thesis: verum end; then consider fb being Real_Sequence such that A33: fb is subsequence of sb * Nseq and A34: fb is convergent and A35: lim fb in [.e,f.] by RCOMP_1:def_3; consider Nseq1 being increasing sequence of NAT such that A36: fb = (sb * Nseq) * Nseq1 by A33, VALUED_0:def_17; set fa = ga * Nseq1; set r = ((lim (ga * Nseq1)) + (lim fb)) / 2; set d0 = dist (A,B); set ff = (1 / 2) (#) ((ga * Nseq1) + fb); A37: ga * Nseq1 is convergent by A28, SEQ_4:16; then A38: (ga * Nseq1) + fb is convergent by A34, SEQ_2:5; then A39: (1 / 2) (#) ((ga * Nseq1) + fb) is convergent by SEQ_2:7; T . 0 meets A by A13; then not A is empty by XBOOLE_1:65; then dist (A,B) > 0 by A1, A14, Th11; then A40: (dist (A,B)) / 2 > 0 by XREAL_1:139; ((lim (ga * Nseq1)) + (lim fb)) / 2 = (1 / 2) * ((lim (ga * Nseq1)) + (lim fb)) .= (1 / 2) * (lim ((ga * Nseq1) + fb)) by A34, A37, SEQ_2:6 .= lim ((1 / 2) (#) ((ga * Nseq1) + fb)) by A38, SEQ_2:8 ; then consider k0 being Element of NAT such that A41: for i being Element of NAT st k0 <= i holds abs ((((1 / 2) (#) ((ga * Nseq1) + fb)) . i) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < (dist (A,B)) / 2 by A39, A40, SEQ_2:def_7; take ((lim (ga * Nseq1)) + (lim fb)) / 2 ; ::_thesis: ( ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.e,f.] & not ((lim (ga * Nseq1)) + (lim fb)) / 2 in A \/ B & ( for i being Element of NAT ex k being Element of NAT st ( i <= k & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . k ) ) ) lim (ga * Nseq1) = lim ga by A28, SEQ_4:17; hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.e,f.] by A29, A35, Th1; ::_thesis: ( not ((lim (ga * Nseq1)) + (lim fb)) / 2 in A \/ B & ( for i being Element of NAT ex k being Element of NAT st ( i <= k & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . k ) ) ) now__::_thesis:_not_((lim_(ga_*_Nseq1))_+_(lim_fb))_/_2_in_A_\/_B set i = Nseq . (Nseq1 . k0); set di = dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))); A42: 2 * (abs ((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) = (abs 2) * (abs ((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) by ABSVALUE:def_1 .= abs (2 * ((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) by COMPLEX1:65 .= abs (((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) ; A43: (ga * Nseq1) . k0 = ga . (Nseq1 . k0) by FUNCT_2:15 .= sa . (Nseq . (Nseq1 . k0)) by A30, FUNCT_2:15 ; T . (Nseq . (Nseq1 . k0)) meets B by A13; then (T . (Nseq . (Nseq1 . k0))) /\ B <> {} by XBOOLE_0:def_7; then A44: not SB . (Nseq . (Nseq1 . k0)) is empty by A16; A45: SB . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ B by A16; then A46: SB . (Nseq . (Nseq1 . k0)) c= B by XBOOLE_1:17; A47: SB . (Nseq . (Nseq1 . k0)) c= T . (Nseq . (Nseq1 . k0)) by A45, XBOOLE_1:17; A48: SA . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ A by A15; then A49: SA . (Nseq . (Nseq1 . k0)) c= A by XBOOLE_1:17; T . (Nseq . (Nseq1 . k0)) meets A by A13; then (T . (Nseq . (Nseq1 . k0))) /\ A <> {} by XBOOLE_0:def_7; then A50: not SA . (Nseq . (Nseq1 . k0)) is empty by A15; then A51: dist (A,B) <= dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) by A44, A49, A46, Th8; (dist (A,B)) / 2 <= (dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))))) / 2 by A50, A44, A49, A46, Th8, XREAL_1:72; then A52: ((dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))))) / 2) + ((dist (A,B)) / 2) <= ((dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))))) / 2) + ((dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))))) / 2) by XREAL_1:6; ((1 / 2) (#) ((ga * Nseq1) + fb)) . k0 = (1 / 2) * (((ga * Nseq1) + fb) . k0) by SEQ_1:9 .= (((ga * Nseq1) + fb) . k0) / 2 .= (((ga * Nseq1) . k0) + (fb . k0)) / 2 by SEQ_1:7 ; then A53: abs (((((ga * Nseq1) . k0) + (fb . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < (dist (A,B)) / 2 by A41; ( not T . (Nseq . (Nseq1 . k0)) is empty & T . (Nseq . (Nseq1 . k0)) is closed_interval ) by A13; then A54: ex a, b being Real st ( a <= b & T . (Nseq . (Nseq1 . k0)) = [.a,b.] ) by MEASURE5:14; A55: sb . (Nseq . (Nseq1 . k0)) in SB . (Nseq . (Nseq1 . k0)) by A24; A56: SA . (Nseq . (Nseq1 . k0)) c= T . (Nseq . (Nseq1 . k0)) by A48, XBOOLE_1:17; A57: fb . k0 = (sb * Nseq) . (Nseq1 . k0) by A36, FUNCT_2:15 .= sb . (Nseq . (Nseq1 . k0)) by FUNCT_2:15 ; 2 * ((dist (A,B)) / 2) = dist (A,B) ; then A58: 2 * (abs ((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) < dist (A,B) by A53, A43, A57, XREAL_1:68; A59: sa . (Nseq . (Nseq1 . k0)) in SA . (Nseq . (Nseq1 . k0)) by A24; then A60: dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) <= abs ((sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0)))) by A55, Th7; A61: now__::_thesis:_((lim_(ga_*_Nseq1))_+_(lim_fb))_/_2_in_T_._(Nseq_._(Nseq1_._k0)) percases ( sa . (Nseq . (Nseq1 . k0)) <= sb . (Nseq . (Nseq1 . k0)) or sb . (Nseq . (Nseq1 . k0)) <= sa . (Nseq . (Nseq1 . k0)) ) ; suppose sa . (Nseq . (Nseq1 . k0)) <= sb . (Nseq . (Nseq1 . k0)) ; ::_thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . (Nseq . (Nseq1 . k0)) then (sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0))) >= 0 by XREAL_1:48; then dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) <= (sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0))) by A60, ABSVALUE:def_1; then dist (A,B) <= (sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0))) by A51, XXREAL_0:2; then abs (((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) <= (sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0))) by A58, A42, XXREAL_0:2; then A62: ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.(sa . (Nseq . (Nseq1 . k0))),(sb . (Nseq . (Nseq1 . k0))).] by RCOMP_1:2; [.(sa . (Nseq . (Nseq1 . k0))),(sb . (Nseq . (Nseq1 . k0))).] c= T . (Nseq . (Nseq1 . k0)) by A54, A59, A55, A56, A47, XXREAL_2:def_12; hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . (Nseq . (Nseq1 . k0)) by A62; ::_thesis: verum end; supposeA63: sb . (Nseq . (Nseq1 . k0)) <= sa . (Nseq . (Nseq1 . k0)) ; ::_thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . (Nseq . (Nseq1 . k0)) A64: abs ((sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0)))) = abs ((sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0)))) by UNIFORM1:11; (sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) >= 0 by A63, XREAL_1:48; then dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) <= (sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) by A60, A64, ABSVALUE:def_1; then dist (A,B) <= (sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) by A51, XXREAL_0:2; then abs (((sb . (Nseq . (Nseq1 . k0))) + (sa . (Nseq . (Nseq1 . k0)))) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) <= (sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) by A58, A42, XXREAL_0:2; then A65: ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.(sb . (Nseq . (Nseq1 . k0))),(sa . (Nseq . (Nseq1 . k0))).] by RCOMP_1:2; [.(sb . (Nseq . (Nseq1 . k0))),(sa . (Nseq . (Nseq1 . k0))).] c= T . (Nseq . (Nseq1 . k0)) by A54, A59, A55, A56, A47, XXREAL_2:def_12; hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . (Nseq . (Nseq1 . k0)) by A65; ::_thesis: verum end; end; end; assume A66: ((lim (ga * Nseq1)) + (lim fb)) / 2 in A \/ B ; ::_thesis: contradiction percases ( ((lim (ga * Nseq1)) + (lim fb)) / 2 in B or ((lim (ga * Nseq1)) + (lim fb)) / 2 in A ) by A66, XBOOLE_0:def_3; supposeA67: ((lim (ga * Nseq1)) + (lim fb)) / 2 in B ; ::_thesis: contradiction SB . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ B by A16; then A68: ((lim (ga * Nseq1)) + (lim fb)) / 2 in SB . (Nseq . (Nseq1 . k0)) by A61, A67, XBOOLE_0:def_4; A69: abs ((((ga * Nseq1) . k0) - (fb . k0)) / 2) = (abs (((ga * Nseq1) . k0) - (fb . k0))) / (abs 2) by COMPLEX1:67 .= (abs (((ga * Nseq1) . k0) - (fb . k0))) / 2 by ABSVALUE:def_1 ; ((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2) = ((((ga * Nseq1) . k0) - (fb . k0)) / 2) + (((((ga * Nseq1) . k0) + (fb . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) ; then A70: abs (((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) <= (abs ((((ga * Nseq1) . k0) - (fb . k0)) / 2)) + (abs (((((ga * Nseq1) . k0) + (fb . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) by COMPLEX1:56; (abs ((((ga * Nseq1) . k0) - (fb . k0)) / 2)) + (abs (((((ga * Nseq1) . k0) + (fb . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) < (abs ((((ga * Nseq1) . k0) - (fb . k0)) / 2)) + ((dist (A,B)) / 2) by A53, XREAL_1:6; then abs (((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < ((abs (((ga * Nseq1) . k0) - (fb . k0))) / 2) + ((dist (A,B)) / 2) by A70, A69, XXREAL_0:2; then abs (((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < ((dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0))))) / 2) + ((dist (A,B)) / 2) by A24, A43, A57; then A71: abs (((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) by A52, XXREAL_0:2; (ga * Nseq1) . k0 in SA . (Nseq . (Nseq1 . k0)) by A24, A43; hence contradiction by A68, A71, Th7; ::_thesis: verum end; supposeA72: ((lim (ga * Nseq1)) + (lim fb)) / 2 in A ; ::_thesis: contradiction SA . (Nseq . (Nseq1 . k0)) = (T . (Nseq . (Nseq1 . k0))) /\ A by A15; then A73: ((lim (ga * Nseq1)) + (lim fb)) / 2 in SA . (Nseq . (Nseq1 . k0)) by A61, A72, XBOOLE_0:def_4; A74: abs (((fb . k0) - ((ga * Nseq1) . k0)) / 2) = (abs ((fb . k0) - ((ga * Nseq1) . k0))) / (abs 2) by COMPLEX1:67 .= (abs ((fb . k0) - ((ga * Nseq1) . k0))) / 2 by ABSVALUE:def_1 ; (fb . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2) = (((fb . k0) - ((ga * Nseq1) . k0)) / 2) + ((((fb . k0) + ((ga * Nseq1) . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) ; then A75: abs ((fb . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) <= (abs (((fb . k0) - ((ga * Nseq1) . k0)) / 2)) + (abs ((((fb . k0) + ((ga * Nseq1) . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) by COMPLEX1:56; A76: abs ((fb . k0) - ((ga * Nseq1) . k0)) = abs (((ga * Nseq1) . k0) - (fb . k0)) by UNIFORM1:11 .= dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) by A24, A43, A57 ; (abs (((fb . k0) - ((ga * Nseq1) . k0)) / 2)) + (abs ((((fb . k0) + ((ga * Nseq1) . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) < (abs (((fb . k0) - ((ga * Nseq1) . k0)) / 2)) + ((dist (A,B)) / 2) by A53, XREAL_1:6; then abs ((fb . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < ((abs ((fb . k0) - ((ga * Nseq1) . k0))) / 2) + ((dist (A,B)) / 2) by A75, A74, XXREAL_0:2; then A77: abs ((fb . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < dist ((SA . (Nseq . (Nseq1 . k0))),(SB . (Nseq . (Nseq1 . k0)))) by A52, A76, XXREAL_0:2; fb . k0 in SB . (Nseq . (Nseq1 . k0)) by A24, A57; hence contradiction by A73, A77, Th7; ::_thesis: verum end; end; end; hence not ((lim (ga * Nseq1)) + (lim fb)) / 2 in A \/ B ; ::_thesis: for i being Element of NAT ex k being Element of NAT st ( i <= k & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . k ) let i be Element of NAT ; ::_thesis: ex k being Element of NAT st ( i <= k & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . k ) set k = max (k0,i); take j = Nseq . (Nseq1 . (max (k0,i))); ::_thesis: ( i <= j & ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . j ) A78: fb . (max (k0,i)) = (sb * Nseq) . (Nseq1 . (max (k0,i))) by A36, FUNCT_2:15 .= sb . j by FUNCT_2:15 ; A79: i <= max (k0,i) by XXREAL_0:25; A80: sb . j in SB . j by A24; T . j meets B by A13; then (T . j) /\ B <> {} by XBOOLE_0:def_7; then A81: not SB . j is empty by A16; A82: dom Nseq = NAT by FUNCT_2:def_1; T . j meets A by A13; then (T . j) /\ A <> {} by XBOOLE_0:def_7; then A83: not SA . j is empty by A15; A84: i <= Nseq . i by SEQM_3:14; A85: SA . j = (T . j) /\ A by A15; then A86: SA . j c= T . j by XBOOLE_1:17; ((1 / 2) (#) ((ga * Nseq1) + fb)) . (max (k0,i)) = (1 / 2) * (((ga * Nseq1) + fb) . (max (k0,i))) by SEQ_1:9 .= (((ga * Nseq1) + fb) . (max (k0,i))) / 2 .= (((ga * Nseq1) . (max (k0,i))) + (fb . (max (k0,i)))) / 2 by SEQ_1:7 ; then A87: abs (((((ga * Nseq1) . (max (k0,i))) + (fb . (max (k0,i)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) < (dist (A,B)) / 2 by A41, XXREAL_0:25; A88: 2 * ((dist (A,B)) / 2) = dist (A,B) ; (ga * Nseq1) . (max (k0,i)) = ga . (Nseq1 . (max (k0,i))) by FUNCT_2:15 .= sa . j by A30, FUNCT_2:15 ; then A89: 2 * (abs ((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) < dist (A,B) by A87, A78, A88, XREAL_1:68; ( not T . j is empty & T . j is closed_interval ) by A13; then A90: ex a, b being Real st ( a <= b & T . j = [.a,b.] ) by MEASURE5:14; A91: SB . j = (T . j) /\ B by A16; then A92: SB . j c= B by XBOOLE_1:17; A93: SB . j c= T . j by A91, XBOOLE_1:17; dom Nseq1 = NAT by FUNCT_2:def_1; then Nseq1 . i <= Nseq1 . (max (k0,i)) by A79, VALUED_0:def_15; then A94: Nseq . (Nseq1 . i) <= j by A82, VALUED_0:def_15; i <= Nseq1 . i by SEQM_3:14; then Nseq . i <= Nseq . (Nseq1 . i) by A82, VALUED_0:def_15; then i <= Nseq . (Nseq1 . i) by A84, XXREAL_0:2; hence i <= j by A94, XXREAL_0:2; ::_thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . j set di = dist ((SA . j),(SB . j)); A95: 2 * (abs ((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) = (abs 2) * (abs ((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) by ABSVALUE:def_1 .= abs (2 * ((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) by COMPLEX1:65 .= abs (((sa . j) + (sb . j)) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) ; SA . j c= A by A85, XBOOLE_1:17; then A96: dist (A,B) <= dist ((SA . j),(SB . j)) by A83, A81, A92, Th8; A97: sa . j in SA . j by A24; then A98: dist ((SA . j),(SB . j)) <= abs ((sb . j) - (sa . j)) by A80, Th7; A99: now__::_thesis:_((lim_(ga_*_Nseq1))_+_(lim_fb))_/_2_in_T_._j percases ( sa . j <= sb . j or sb . j <= sa . j ) ; suppose sa . j <= sb . j ; ::_thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . j then (sb . j) - (sa . j) >= 0 by XREAL_1:48; then dist ((SA . j),(SB . j)) <= (sb . j) - (sa . j) by A98, ABSVALUE:def_1; then dist (A,B) <= (sb . j) - (sa . j) by A96, XXREAL_0:2; then abs (((sa . j) + (sb . j)) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) <= (sb . j) - (sa . j) by A89, A95, XXREAL_0:2; then A100: ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.(sa . j),(sb . j).] by RCOMP_1:2; [.(sa . j),(sb . j).] c= T . j by A90, A97, A80, A86, A93, XXREAL_2:def_12; hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . j by A100; ::_thesis: verum end; supposeA101: sb . j <= sa . j ; ::_thesis: ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . j A102: abs ((sb . j) - (sa . j)) = abs ((sa . j) - (sb . j)) by UNIFORM1:11; (sa . j) - (sb . j) >= 0 by A101, XREAL_1:48; then dist ((SA . j),(SB . j)) <= (sa . j) - (sb . j) by A98, A102, ABSVALUE:def_1; then dist (A,B) <= (sa . j) - (sb . j) by A96, XXREAL_0:2; then abs (((sb . j) + (sa . j)) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) <= (sa . j) - (sb . j) by A89, A95, XXREAL_0:2; then A103: ((lim (ga * Nseq1)) + (lim fb)) / 2 in [.(sb . j),(sa . j).] by RCOMP_1:2; [.(sb . j),(sa . j).] c= T . j by A90, A97, A80, A86, A93, XXREAL_2:def_12; hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in T . j by A103; ::_thesis: verum end; end; end; T . j c= S . j by A13; hence ((lim (ga * Nseq1)) + (lim fb)) / 2 in S . j by A99; ::_thesis: verum end; theorem Th13: :: JCT_MISC:13 for S being closed Subset of (TOP-REAL 2) st S is bounded holds proj2 .: S is closed proof let S be closed Subset of (TOP-REAL 2); ::_thesis: ( S is bounded implies proj2 .: S is closed ) assume S is bounded ; ::_thesis: proj2 .: S is closed then Cl (proj2 .: S) = proj2 .: (Cl S) by TOPREAL6:84 .= proj2 .: S by PRE_TOPC:22 ; hence proj2 .: S is closed ; ::_thesis: verum end; theorem Th14: :: JCT_MISC:14 for S being Subset of (TOP-REAL 2) st S is bounded holds proj2 .: S is real-bounded proof let S be Subset of (TOP-REAL 2); ::_thesis: ( S is bounded implies proj2 .: S is real-bounded ) assume S is bounded ; ::_thesis: proj2 .: S is real-bounded then reconsider C = S as bounded Subset of (Euclid 2) by JORDAN2C:11; consider r being Real, x being Point of (Euclid 2) such that A1: 0 < r and A2: C c= Ball (x,r) by METRIC_6:def_3; reconsider P = Ball (x,r) as Subset of (TOP-REAL 2) by TOPREAL3:8; reconsider p = x as Point of (TOP-REAL 2) by TOPREAL3:8; set t = max ((abs ((p `2) - r)),(abs ((p `2) + r))); now__::_thesis:_(_abs_((p_`2)_-_r)_<=_0_implies_not_abs_((p_`2)_+_r)_<=_0_) assume that A3: abs ((p `2) - r) <= 0 and A4: abs ((p `2) + r) <= 0 ; ::_thesis: contradiction abs ((p `2) - r) = 0 by A3, COMPLEX1:46; then abs (r - (p `2)) = 0 by UNIFORM1:11; then A5: r - (p `2) = 0 by ABSVALUE:2; abs ((p `2) + r) = 0 by A4, COMPLEX1:46; hence contradiction by A1, A5, ABSVALUE:2; ::_thesis: verum end; then A6: max ((abs ((p `2) - r)),(abs ((p `2) + r))) > 0 by XXREAL_0:30; A7: proj2 .: P = ].((p `2) - r),((p `2) + r).[ by TOPREAL6:44; for s being real number st s in proj2 .: S holds abs s < max ((abs ((p `2) - r)),(abs ((p `2) + r))) proof let s be real number ; ::_thesis: ( s in proj2 .: S implies abs s < max ((abs ((p `2) - r)),(abs ((p `2) + r))) ) proj2 .: S c= proj2 .: P by A2, RELAT_1:123; hence ( s in proj2 .: S implies abs s < max ((abs ((p `2) - r)),(abs ((p `2) + r))) ) by A7, Th3; ::_thesis: verum end; hence proj2 .: S is real-bounded by A6, SEQ_4:4; ::_thesis: verum end; theorem :: JCT_MISC:15 for S being compact Subset of (TOP-REAL 2) holds proj2 .: S is compact proof let S be compact Subset of (TOP-REAL 2); ::_thesis: proj2 .: S is compact proj2 .: S is closed by Th13; hence proj2 .: S is compact by Th14, RCOMP_1:11; ::_thesis: verum end;