:: RCOMP_1 semantic presentation begin definition let g, s be real number ; :: original: [. redefine func[.g,s.] -> Subset of REAL equals :: RCOMP_1:def 1 { r where r is Real : ( g <= r & r <= s ) } ; coherence [.g,s.] is Subset of REAL proof now__::_thesis:_for_x_being_set_st_x_in_[.g,s.]_holds_ x_in_REAL let x be set ; ::_thesis: ( x in [.g,s.] implies x in REAL ) assume x in [.g,s.] ; ::_thesis: x in REAL then A1: ex r being Element of ExtREAL st ( x = r & g <= r & r <= s ) ; ( g in REAL & s in REAL ) by XREAL_0:def_1; hence x in REAL by A1, XXREAL_0:45; ::_thesis: verum end; hence [.g,s.] is Subset of REAL by TARSKI:def_3; ::_thesis: verum end; compatibility for b1 being Subset of REAL holds ( b1 = [.g,s.] iff b1 = { r where r is Real : ( g <= r & r <= s ) } ) proof set Y = { r where r is Real : ( g <= r & r <= s ) } ; let X be Subset of REAL; ::_thesis: ( X = [.g,s.] iff X = { r where r is Real : ( g <= r & r <= s ) } ) A2: [.g,s.] c= { r where r is Real : ( g <= r & r <= s ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [.g,s.] or x in { r where r is Real : ( g <= r & r <= s ) } ) assume x in [.g,s.] ; ::_thesis: x in { r where r is Real : ( g <= r & r <= s ) } then consider r being Element of ExtREAL such that A3: x = r and A4: ( g <= r & r <= s ) ; ( g in REAL & s in REAL ) by XREAL_0:def_1; then r in REAL by A4, XXREAL_0:45; hence x in { r where r is Real : ( g <= r & r <= s ) } by A3, A4; ::_thesis: verum end; { r where r is Real : ( g <= r & r <= s ) } c= [.g,s.] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { r where r is Real : ( g <= r & r <= s ) } or x in [.g,s.] ) assume x in { r where r is Real : ( g <= r & r <= s ) } ; ::_thesis: x in [.g,s.] then consider r being Element of REAL such that A5: ( x = r & g <= r & r <= s ) ; r in REAL ; hence x in [.g,s.] by A5, NUMBERS:31; ::_thesis: verum end; hence ( X = [.g,s.] iff X = { r where r is Real : ( g <= r & r <= s ) } ) by A2, XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem defines [. RCOMP_1:def_1_:_ for g, s being real number holds [.g,s.] = { r where r is Real : ( g <= r & r <= s ) } ; definition let g, s be ext-real number ; :: original: ]. redefine func].g,s.[ -> Subset of REAL equals :: RCOMP_1:def 2 { r where r is Real : ( g < r & r < s ) } ; coherence ].g,s.[ is Subset of REAL proof now__::_thesis:_for_x_being_set_st_x_in_].g,s.[_holds_ x_in_REAL let x be set ; ::_thesis: ( x in ].g,s.[ implies x in REAL ) assume x in ].g,s.[ ; ::_thesis: x in REAL then ex r being Element of ExtREAL st ( x = r & g < r & r < s ) ; hence x in REAL by XXREAL_0:48; ::_thesis: verum end; hence ].g,s.[ is Subset of REAL by TARSKI:def_3; ::_thesis: verum end; compatibility for b1 being Subset of REAL holds ( b1 = ].g,s.[ iff b1 = { r where r is Real : ( g < r & r < s ) } ) proof set Y = { r where r is Real : ( g < r & r < s ) } ; let X be Subset of REAL; ::_thesis: ( X = ].g,s.[ iff X = { r where r is Real : ( g < r & r < s ) } ) A1: { r where r is Real : ( g < r & r < s ) } c= ].g,s.[ proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { r where r is Real : ( g < r & r < s ) } or x in ].g,s.[ ) assume x in { r where r is Real : ( g < r & r < s ) } ; ::_thesis: x in ].g,s.[ then consider r being Element of REAL such that A2: ( x = r & g < r & r < s ) ; r in REAL ; hence x in ].g,s.[ by A2, NUMBERS:31; ::_thesis: verum end; ].g,s.[ c= { r where r is Real : ( g < r & r < s ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ].g,s.[ or x in { r where r is Real : ( g < r & r < s ) } ) assume x in ].g,s.[ ; ::_thesis: x in { r where r is Real : ( g < r & r < s ) } then consider r being Element of ExtREAL such that A3: x = r and A4: ( g < r & r < s ) ; r in REAL by A4, XXREAL_0:48; hence x in { r where r is Real : ( g < r & r < s ) } by A3, A4; ::_thesis: verum end; hence ( X = ].g,s.[ iff X = { r where r is Real : ( g < r & r < s ) } ) by A1, XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem defines ]. RCOMP_1:def_2_:_ for g, s being ext-real number holds ].g,s.[ = { r where r is Real : ( g < r & r < s ) } ; theorem Th1: :: RCOMP_1:1 for r, p, g being real number holds ( r in ].(p - g),(p + g).[ iff abs (r - p) < g ) proof let r, p, g be real number ; ::_thesis: ( r in ].(p - g),(p + g).[ iff abs (r - p) < g ) thus ( r in ].(p - g),(p + g).[ implies abs (r - p) < g ) ::_thesis: ( abs (r - p) < g implies r in ].(p - g),(p + g).[ ) proof assume r in ].(p - g),(p + g).[ ; ::_thesis: abs (r - p) < g then A1: ex s being Real st ( r = s & p - g < s & s < p + g ) ; then p + (- g) < r ; then A2: - g < r - p by XREAL_1:20; r - p < g by A1, XREAL_1:19; hence abs (r - p) < g by A2, SEQ_2:1; ::_thesis: verum end; assume A3: abs (r - p) < g ; ::_thesis: r in ].(p - g),(p + g).[ then r - p < g by SEQ_2:1; then A4: r < p + g by XREAL_1:19; - g < r - p by A3, SEQ_2:1; then ( r is Real & p + (- g) < r ) by XREAL_0:def_1, XREAL_1:20; hence r in ].(p - g),(p + g).[ by A4; ::_thesis: verum end; theorem :: RCOMP_1:2 for r, p, g being real number holds ( r in [.p,g.] iff abs ((p + g) - (2 * r)) <= g - p ) proof let r, p, g be real number ; ::_thesis: ( r in [.p,g.] iff abs ((p + g) - (2 * r)) <= g - p ) thus ( r in [.p,g.] implies abs ((p + g) - (2 * r)) <= g - p ) ::_thesis: ( abs ((p + g) - (2 * r)) <= g - p implies r in [.p,g.] ) proof assume r in [.p,g.] ; ::_thesis: abs ((p + g) - (2 * r)) <= g - p then A1: ex s being Real st ( s = r & p <= s & s <= g ) ; then 2 * r <= 2 * g by XREAL_1:64; then - (2 * r) >= - (2 * g) by XREAL_1:24; then (p + g) + (- (2 * r)) >= (p + g) + (- (2 * g)) by XREAL_1:7; then A2: (p + g) - (2 * r) >= - (g - p) ; 2 * p <= 2 * r by A1, XREAL_1:64; then - (2 * p) >= - (2 * r) by XREAL_1:24; then (p + g) + (- (2 * p)) >= (p + g) + (- (2 * r)) by XREAL_1:7; hence abs ((p + g) - (2 * r)) <= g - p by A2, ABSVALUE:5; ::_thesis: verum end; assume A3: abs ((p + g) - (2 * r)) <= g - p ; ::_thesis: r in [.p,g.] then (p + g) - (2 * r) >= - (g - p) by ABSVALUE:5; then p + g >= (p - g) + (2 * r) by XREAL_1:19; then (p + g) - (p - g) >= 2 * r by XREAL_1:19; then A4: (1 / 2) * (2 * g) >= (1 / 2) * (2 * r) by XREAL_1:64; g - p >= (p + g) - (2 * r) by A3, ABSVALUE:5; then (2 * r) + (g - p) >= p + g by XREAL_1:20; then 2 * r >= (p + g) - (g - p) by XREAL_1:20; then (1 / 2) * (2 * r) >= (1 / 2) * (2 * p) by XREAL_1:64; hence r in [.p,g.] by A4; ::_thesis: verum end; theorem :: RCOMP_1:3 for r, p, g being real number holds ( r in ].p,g.[ iff abs ((p + g) - (2 * r)) < g - p ) proof let r, p, g be real number ; ::_thesis: ( r in ].p,g.[ iff abs ((p + g) - (2 * r)) < g - p ) thus ( r in ].p,g.[ implies abs ((p + g) - (2 * r)) < g - p ) ::_thesis: ( abs ((p + g) - (2 * r)) < g - p implies r in ].p,g.[ ) proof assume r in ].p,g.[ ; ::_thesis: abs ((p + g) - (2 * r)) < g - p then A1: ex s being Real st ( s = r & p < s & s < g ) ; then 2 * r < 2 * g by XREAL_1:68; then - (2 * r) > - (2 * g) by XREAL_1:24; then (p + g) + (- (2 * r)) > (p + g) + (- (2 * g)) by XREAL_1:6; then A2: (p + g) - (2 * r) > - (g - p) ; 2 * p < 2 * r by A1, XREAL_1:68; then - (2 * p) > - (2 * r) by XREAL_1:24; then (p + g) + (- (2 * p)) > (p + g) + (- (2 * r)) by XREAL_1:6; hence abs ((p + g) - (2 * r)) < g - p by A2, SEQ_2:1; ::_thesis: verum end; assume A3: abs ((p + g) - (2 * r)) < g - p ; ::_thesis: r in ].p,g.[ then (p + g) - (2 * r) > - (g - p) by SEQ_2:1; then p + g > (p - g) + (2 * r) by XREAL_1:20; then (p + g) - (p - g) > 2 * r by XREAL_1:20; then A4: (1 / 2) * (2 * g) > (1 / 2) * (2 * r) by XREAL_1:68; g - p > (p + g) - (2 * r) by A3, SEQ_2:1; then (2 * r) + (g - p) > p + g by XREAL_1:19; then 2 * r > (p + g) - (g - p) by XREAL_1:19; then (1 / 2) * (2 * r) > (1 / 2) * (2 * p) by XREAL_1:68; hence r in ].p,g.[ by A4; ::_thesis: verum end; definition let X be Subset of REAL; attrX is compact means :Def3: :: RCOMP_1:def 3 for s1 being Real_Sequence st rng s1 c= X holds ex s2 being Real_Sequence st ( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ); end; :: deftheorem Def3 defines compact RCOMP_1:def_3_:_ for X being Subset of REAL holds ( X is compact iff for s1 being Real_Sequence st rng s1 c= X holds ex s2 being Real_Sequence st ( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) ); definition let X be Subset of REAL; attrX is closed means :Def4: :: RCOMP_1:def 4 for s1 being Real_Sequence st rng s1 c= X & s1 is convergent holds lim s1 in X; end; :: deftheorem Def4 defines closed RCOMP_1:def_4_:_ for X being Subset of REAL holds ( X is closed iff for s1 being Real_Sequence st rng s1 c= X & s1 is convergent holds lim s1 in X ); definition let X be Subset of REAL; attrX is open means :Def5: :: RCOMP_1:def 5 X ` is closed ; end; :: deftheorem Def5 defines open RCOMP_1:def_5_:_ for X being Subset of REAL holds ( X is open iff X ` is closed ); theorem Th4: :: RCOMP_1:4 for s, g being real number for s1 being Real_Sequence st rng s1 c= [.s,g.] holds s1 is bounded proof let s, g be real number ; ::_thesis: for s1 being Real_Sequence st rng s1 c= [.s,g.] holds s1 is bounded let s1 be Real_Sequence; ::_thesis: ( rng s1 c= [.s,g.] implies s1 is bounded ) assume A1: rng s1 c= [.s,g.] ; ::_thesis: s1 is bounded thus s1 is bounded_above :: according to SEQ_2:def_8 ::_thesis: s1 is bounded_below proof take r = g + 1; :: according to SEQ_2:def_3 ::_thesis: for b1 being Element of NAT holds not r <= s1 . b1 A2: for t being real number st t in rng s1 holds t < r proof let t be real number ; ::_thesis: ( t in rng s1 implies t < r ) assume t in rng s1 ; ::_thesis: t < r then t in [.s,g.] by A1; then A3: ex p being Real st ( t = p & s <= p & p <= g ) ; g < r by XREAL_1:29; hence t < r by A3, XXREAL_0:2; ::_thesis: verum end; for n being Element of NAT holds s1 . n < r proof let n be Element of NAT ; ::_thesis: s1 . n < r n in NAT ; then n in dom s1 by FUNCT_2:def_1; then s1 . n in rng s1 by FUNCT_1:def_3; hence s1 . n < r by A2; ::_thesis: verum end; hence for b1 being Element of NAT holds not r <= s1 . b1 ; ::_thesis: verum end; thus s1 is bounded_below ::_thesis: verum proof take r = s - 1; :: according to SEQ_2:def_4 ::_thesis: for b1 being Element of NAT holds not s1 . b1 <= r A4: r + 1 = s - (1 - 1) ; A5: for t being real number st t in rng s1 holds r < t proof let t be real number ; ::_thesis: ( t in rng s1 implies r < t ) assume t in rng s1 ; ::_thesis: r < t then t in [.s,g.] by A1; then A6: ex p being Real st ( t = p & s <= p & p <= g ) ; r < s by A4, XREAL_1:29; hence r < t by A6, XXREAL_0:2; ::_thesis: verum end; for n being Element of NAT holds r < s1 . n proof let n be Element of NAT ; ::_thesis: r < s1 . n n in NAT ; then n in dom s1 by FUNCT_2:def_1; then s1 . n in rng s1 by FUNCT_1:def_3; hence r < s1 . n by A5; ::_thesis: verum end; hence for b1 being Element of NAT holds not s1 . b1 <= r ; ::_thesis: verum end; end; theorem Th5: :: RCOMP_1:5 for s, g being real number holds [.s,g.] is closed proof let s, g be real number ; ::_thesis: [.s,g.] is closed for s1 being Real_Sequence st rng s1 c= [.s,g.] & s1 is convergent holds lim s1 in [.s,g.] proof let s1 be Real_Sequence; ::_thesis: ( rng s1 c= [.s,g.] & s1 is convergent implies lim s1 in [.s,g.] ) assume that A1: rng s1 c= [.s,g.] and A2: s1 is convergent ; ::_thesis: lim s1 in [.s,g.] A3: s <= lim s1 proof s in REAL by XREAL_0:def_1; then reconsider s2 = NAT --> s as Real_Sequence by FUNCOP_1:45; A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_s2_._n_<=_s1_._n let n be Element of NAT ; ::_thesis: s2 . n <= s1 . n n in NAT ; then n in dom s1 by FUNCT_2:def_1; then s1 . n in rng s1 by FUNCT_1:def_3; then s1 . n in [.s,g.] by A1; then ex p being Real st ( s1 . n = p & s <= p & p <= g ) ; hence s2 . n <= s1 . n by FUNCOP_1:7; ::_thesis: verum end; s2 . 0 = s by FUNCOP_1:7; then lim s2 = s by SEQ_4:25; hence s <= lim s1 by A2, A4, SEQ_2:18; ::_thesis: verum end; lim s1 <= g proof g in REAL by XREAL_0:def_1; then reconsider s2 = NAT --> g as Real_Sequence by FUNCOP_1:45; A5: now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_<=_s2_._n let n be Element of NAT ; ::_thesis: s1 . n <= s2 . n n in NAT ; then n in dom s1 by FUNCT_2:def_1; then s1 . n in rng s1 by FUNCT_1:def_3; then s1 . n in [.s,g.] by A1; then ex p being Real st ( s1 . n = p & s <= p & p <= g ) ; hence s1 . n <= s2 . n by FUNCOP_1:7; ::_thesis: verum end; s2 . 0 = g by FUNCOP_1:7; then lim s2 = g by SEQ_4:25; hence lim s1 <= g by A2, A5, SEQ_2:18; ::_thesis: verum end; hence lim s1 in [.s,g.] by A3; ::_thesis: verum end; hence [.s,g.] is closed by Def4; ::_thesis: verum end; theorem :: RCOMP_1:6 for s, g being real number holds [.s,g.] is compact proof let s, g be real number ; ::_thesis: [.s,g.] is compact for s1 being Real_Sequence st rng s1 c= [.s,g.] holds ex s2 being Real_Sequence st ( s2 is subsequence of s1 & s2 is convergent & lim s2 in [.s,g.] ) proof let s1 be Real_Sequence; ::_thesis: ( rng s1 c= [.s,g.] implies ex s2 being Real_Sequence st ( s2 is subsequence of s1 & s2 is convergent & lim s2 in [.s,g.] ) ) A1: [.s,g.] is closed by Th5; assume A2: rng s1 c= [.s,g.] ; ::_thesis: ex s2 being Real_Sequence st ( s2 is subsequence of s1 & s2 is convergent & lim s2 in [.s,g.] ) then consider s2 being Real_Sequence such that A3: s2 is subsequence of s1 and A4: s2 is convergent by Th4, SEQ_4:40; take s2 ; ::_thesis: ( s2 is subsequence of s1 & s2 is convergent & lim s2 in [.s,g.] ) ex Nseq being increasing sequence of NAT st s2 = s1 * Nseq by A3, VALUED_0:def_17; then rng s2 c= rng s1 by RELAT_1:26; then rng s2 c= [.s,g.] by A2, XBOOLE_1:1; hence ( s2 is subsequence of s1 & s2 is convergent & lim s2 in [.s,g.] ) by A3, A4, A1, Def4; ::_thesis: verum end; hence [.s,g.] is compact by Def3; ::_thesis: verum end; theorem Th7: :: RCOMP_1:7 for p, q being real number holds ].p,q.[ is open proof let p, q be real number ; ::_thesis: ].p,q.[ is open defpred S1[ Real] means ( $1 <= p or q <= $1 ); consider X being Subset of REAL such that A1: for r being Real holds ( r in X iff S1[r] ) from SUBSET_1:sch_3(); now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_X_&_s1_is_convergent_holds_ lim_s1_in_X let s1 be Real_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent implies lim s1 in X ) assume that A2: rng s1 c= X and A3: s1 is convergent ; ::_thesis: lim s1 in X ( lim s1 <= p or q <= lim s1 ) proof assume A4: ( not lim s1 <= p & not q <= lim s1 ) ; ::_thesis: contradiction then 0 < (lim s1) - p by XREAL_1:50; then consider n1 being Element of NAT such that A5: for m being Element of NAT st n1 <= m holds abs ((s1 . m) - (lim s1)) < (lim s1) - p by A3, SEQ_2:def_7; 0 < q - (lim s1) by A4, XREAL_1:50; then consider n being Element of NAT such that A6: for m being Element of NAT st n <= m holds abs ((s1 . m) - (lim s1)) < q - (lim s1) by A3, SEQ_2:def_7; consider k being Element of NAT such that A7: max (n,n1) < k by SEQ_4:3; n1 <= max (n,n1) by XXREAL_0:25; then n1 <= k by A7, XXREAL_0:2; then A8: abs ((s1 . k) - (lim s1)) < (lim s1) - p by A5; - (abs ((s1 . k) - (lim s1))) <= (s1 . k) - (lim s1) by ABSVALUE:4; then - ((s1 . k) - (lim s1)) <= - (- (abs ((s1 . k) - (lim s1)))) by XREAL_1:24; then - ((s1 . k) - (lim s1)) < (lim s1) - p by A8, XXREAL_0:2; then - ((lim s1) - p) < - (- ((s1 . k) - (lim s1))) by XREAL_1:24; then p - (lim s1) < (s1 . k) - (lim s1) ; then A9: p < s1 . k by XREAL_1:9; n <= max (n,n1) by XXREAL_0:25; then n <= k by A7, XXREAL_0:2; then ( (s1 . k) - (lim s1) <= abs ((s1 . k) - (lim s1)) & abs ((s1 . k) - (lim s1)) < q - (lim s1) ) by A6, ABSVALUE:4; then (s1 . k) - (lim s1) < q - (lim s1) by XXREAL_0:2; then A10: s1 . k < q by XREAL_1:9; dom s1 = NAT by FUNCT_2:def_1; then s1 . k in rng s1 by FUNCT_1:def_3; hence contradiction by A1, A2, A10, A9; ::_thesis: verum end; hence lim s1 in X by A1; ::_thesis: verum end; then A11: X is closed by Def4; now__::_thesis:_for_r_being_real_number_st_r_in_].p,q.[_`_holds_ r_in_X let r be real number ; ::_thesis: ( r in ].p,q.[ ` implies r in X ) A12: r is Real by XREAL_0:def_1; assume r in ].p,q.[ ` ; ::_thesis: r in X then not r in ].p,q.[ by XBOOLE_0:def_5; then ( r <= p or q <= r ) by A12; hence r in X by A1, A12; ::_thesis: verum end; then A13: ].p,q.[ ` c= X by MEMBERED:def_9; now__::_thesis:_for_r_being_real_number_st_r_in_X_holds_ r_in_].p,q.[_` let r be real number ; ::_thesis: ( r in X implies r in ].p,q.[ ` ) assume r in X ; ::_thesis: r in ].p,q.[ ` then for s being Real holds ( not s = r or not p < s or not s < q ) by A1; then ( r is Real & not r in ].p,q.[ ) by XREAL_0:def_1; hence r in ].p,q.[ ` by XBOOLE_0:def_5; ::_thesis: verum end; then X c= ].p,q.[ ` by MEMBERED:def_9; then ].p,q.[ ` = X by A13, XBOOLE_0:def_10; hence ].p,q.[ is open by A11, Def5; ::_thesis: verum end; registration let p, q be real number ; cluster].p,q.[ -> open for Subset of REAL; coherence for b1 being Subset of REAL st b1 = ].p,q.[ holds b1 is open by Th7; cluster[.p,q.] -> closed for Subset of REAL; coherence for b1 being Subset of REAL st b1 = [.p,q.] holds b1 is closed by Th5; end; theorem Th8: :: RCOMP_1:8 for X being Subset of REAL st X is compact holds X is closed proof let X be Subset of REAL; ::_thesis: ( X is compact implies X is closed ) assume A1: X is compact ; ::_thesis: X is closed assume not X is closed ; ::_thesis: contradiction then consider s1 being Real_Sequence such that A2: rng s1 c= X and A3: ( s1 is convergent & not lim s1 in X ) by Def4; ex s2 being Real_Sequence st ( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) by A1, A2, Def3; hence contradiction by A3, SEQ_4:17; ::_thesis: verum end; registration cluster compact -> closed for Element of K19(REAL); coherence for b1 being Subset of REAL st b1 is compact holds b1 is closed by Th8; end; theorem Th9: :: RCOMP_1:9 for s1 being Real_Sequence for X being Subset of REAL st ( for p being real number st p in X holds ex r being real number ex n being Element of NAT st ( 0 < r & ( for m being Element of NAT st n < m holds r < abs ((s1 . m) - p) ) ) ) holds for s2 being Real_Sequence st s2 is subsequence of s1 & s2 is convergent holds not lim s2 in X proof let s1 be Real_Sequence; ::_thesis: for X being Subset of REAL st ( for p being real number st p in X holds ex r being real number ex n being Element of NAT st ( 0 < r & ( for m being Element of NAT st n < m holds r < abs ((s1 . m) - p) ) ) ) holds for s2 being Real_Sequence st s2 is subsequence of s1 & s2 is convergent holds not lim s2 in X let X be Subset of REAL; ::_thesis: ( ( for p being real number st p in X holds ex r being real number ex n being Element of NAT st ( 0 < r & ( for m being Element of NAT st n < m holds r < abs ((s1 . m) - p) ) ) ) implies for s2 being Real_Sequence st s2 is subsequence of s1 & s2 is convergent holds not lim s2 in X ) assume that A1: for p being real number st p in X holds ex r being real number ex n being Element of NAT st ( 0 < r & ( for m being Element of NAT st n < m holds r < abs ((s1 . m) - p) ) ) and A2: ex s2 being Real_Sequence st ( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) ; ::_thesis: contradiction consider s2 being Real_Sequence such that A3: s2 is subsequence of s1 and A4: s2 is convergent and A5: lim s2 in X by A2; consider r being real number , n being Element of NAT such that A6: 0 < r and A7: for m being Element of NAT st n < m holds r < abs ((s1 . m) - (lim s2)) by A1, A5; consider n1 being Element of NAT such that A8: for m being Element of NAT st n1 <= m holds abs ((s2 . m) - (lim s2)) < r by A4, A6, SEQ_2:def_7; consider NS being increasing sequence of NAT such that A9: s2 = s1 * NS by A3, VALUED_0:def_17; set k = (n + 1) + n1; abs (((s1 * NS) . ((n + 1) + n1)) - (lim s2)) < r by A8, A9, NAT_1:11; then A10: abs ((s1 . (NS . ((n + 1) + n1))) - (lim s2)) < r by FUNCT_2:15; n + 1 <= (n + 1) + n1 by NAT_1:11; then A11: n < (n + 1) + n1 by NAT_1:13; (n + 1) + n1 <= NS . ((n + 1) + n1) by SEQM_3:14; then n < NS . ((n + 1) + n1) by A11, XXREAL_0:2; hence contradiction by A7, A10; ::_thesis: verum end; theorem Th10: :: RCOMP_1:10 for X being Subset of REAL st X is compact holds X is real-bounded proof let X be Subset of REAL; ::_thesis: ( X is compact implies X is real-bounded ) assume A1: X is compact ; ::_thesis: X is real-bounded assume A2: not X is real-bounded ; ::_thesis: contradiction percases ( not X is bounded_above or not X is bounded_below ) by A2; supposeA3: not X is bounded_above ; ::_thesis: contradiction defpred S1[ Element of NAT , Element of REAL ] means ex q being real number st ( q = $2 & q in X & $1 < q ); A4: for n being Element of NAT ex p being Element of REAL st S1[n,p] proof let n be Element of NAT ; ::_thesis: ex p being Element of REAL st S1[n,p] n is not UpperBound of X by A3, XXREAL_2:def_10; then consider t being ext-real number such that A5: ( t in X & n < t ) by XXREAL_2:def_1; take t ; ::_thesis: ( t is Element of REAL & S1[n,t] ) thus ( t is Element of REAL & S1[n,t] ) by A5; ::_thesis: verum end; consider f being Function of NAT,REAL such that A6: for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch_3(A4); A7: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_f_._n_in_X_&_n_<_f_._n_) let n be Element of NAT ; ::_thesis: ( f . n in X & n < f . n ) ex q being real number st ( q = f . n & q in X & n < q ) by A6; hence ( f . n in X & n < f . n ) ; ::_thesis: verum end; A8: for p being real number st p in X holds ex r being real number ex n being Element of NAT st ( 0 < r & ( for m being Element of NAT st n < m holds r < abs ((f . m) - p) ) ) proof let p be real number ; ::_thesis: ( p in X implies ex r being real number ex n being Element of NAT st ( 0 < r & ( for m being Element of NAT st n < m holds r < abs ((f . m) - p) ) ) ) assume p in X ; ::_thesis: ex r being real number ex n being Element of NAT st ( 0 < r & ( for m being Element of NAT st n < m holds r < abs ((f . m) - p) ) ) consider q being real number such that A9: q = 1 ; take r = q; ::_thesis: ex n being Element of NAT st ( 0 < r & ( for m being Element of NAT st n < m holds r < abs ((f . m) - p) ) ) consider k being Element of NAT such that A10: p + 1 < k by SEQ_4:3; take n = k; ::_thesis: ( 0 < r & ( for m being Element of NAT st n < m holds r < abs ((f . m) - p) ) ) thus 0 < r by A9; ::_thesis: for m being Element of NAT st n < m holds r < abs ((f . m) - p) let m be Element of NAT ; ::_thesis: ( n < m implies r < abs ((f . m) - p) ) assume n < m ; ::_thesis: r < abs ((f . m) - p) then p + 1 < m by A10, XXREAL_0:2; then p + 1 < f . m by A7, XXREAL_0:2; then 1 < (f . m) - p by XREAL_1:20; hence r < abs ((f . m) - p) by A9, ABSVALUE:def_1; ::_thesis: verum end; rng f c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in X ) assume x in rng f ; ::_thesis: x in X then consider y being set such that A11: y in dom f and A12: x = f . y by FUNCT_1:def_3; reconsider y = y as Element of NAT by A11, FUNCT_2:def_1; f . y in X by A7; hence x in X by A12; ::_thesis: verum end; then ex s2 being Real_Sequence st ( s2 is subsequence of f & s2 is convergent & lim s2 in X ) by A1, Def3; hence contradiction by A8, Th9; ::_thesis: verum end; supposeA13: not X is bounded_below ; ::_thesis: contradiction defpred S1[ Element of NAT , Element of REAL ] means ex q being real number st ( q = $2 & q in X & q < - $1 ); A14: for n being Element of NAT ex p being Element of REAL st S1[n,p] proof let n be Element of NAT ; ::_thesis: ex p being Element of REAL st S1[n,p] - n is not LowerBound of X by A13, XXREAL_2:def_9; then consider t being ext-real number such that A15: ( t in X & t < - n ) by XXREAL_2:def_2; take t ; ::_thesis: ( t is Element of REAL & S1[n,t] ) thus ( t is Element of REAL & S1[n,t] ) by A15; ::_thesis: verum end; consider f being Function of NAT,REAL such that A16: for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch_3(A14); A17: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_f_._n_in_X_&_f_._n_<_-_n_) let n be Element of NAT ; ::_thesis: ( f . n in X & f . n < - n ) ex q being real number st ( q = f . n & q in X & q < - n ) by A16; hence ( f . n in X & f . n < - n ) ; ::_thesis: verum end; A18: for p being real number st p in X holds ex r being real number ex n being Element of NAT st ( 0 < r & ( for m being Element of NAT st n < m holds r < abs ((f . m) - p) ) ) proof let p be real number ; ::_thesis: ( p in X implies ex r being real number ex n being Element of NAT st ( 0 < r & ( for m being Element of NAT st n < m holds r < abs ((f . m) - p) ) ) ) assume p in X ; ::_thesis: ex r being real number ex n being Element of NAT st ( 0 < r & ( for m being Element of NAT st n < m holds r < abs ((f . m) - p) ) ) consider q being real number such that A19: q = 1 ; take r = q; ::_thesis: ex n being Element of NAT st ( 0 < r & ( for m being Element of NAT st n < m holds r < abs ((f . m) - p) ) ) consider k being Element of NAT such that A20: abs (p - 1) < k by SEQ_4:3; take n = k; ::_thesis: ( 0 < r & ( for m being Element of NAT st n < m holds r < abs ((f . m) - p) ) ) thus 0 < r by A19; ::_thesis: for m being Element of NAT st n < m holds r < abs ((f . m) - p) let m be Element of NAT ; ::_thesis: ( n < m implies r < abs ((f . m) - p) ) assume n < m ; ::_thesis: r < abs ((f . m) - p) then A21: - m < - n by XREAL_1:24; - k < p - 1 by A20, SEQ_2:1; then - m < p - 1 by A21, XXREAL_0:2; then f . m < p - 1 by A17, XXREAL_0:2; then (f . m) + 1 < p by XREAL_1:20; then 1 < p - (f . m) by XREAL_1:20; then r < abs (- ((f . m) - p)) by A19, ABSVALUE:def_1; hence r < abs ((f . m) - p) by COMPLEX1:52; ::_thesis: verum end; rng f c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in X ) assume x in rng f ; ::_thesis: x in X then consider y being set such that A22: y in dom f and A23: x = f . y by FUNCT_1:def_3; reconsider y = y as Element of NAT by A22, FUNCT_2:def_1; f . y in X by A17; hence x in X by A23; ::_thesis: verum end; then ex s2 being Real_Sequence st ( s2 is subsequence of f & s2 is convergent & lim s2 in X ) by A1, Def3; hence contradiction by A18, Th9; ::_thesis: verum end; end; end; theorem :: RCOMP_1:11 for X being Subset of REAL st X is real-bounded & X is closed holds X is compact proof let X be Subset of REAL; ::_thesis: ( X is real-bounded & X is closed implies X is compact ) assume that A1: X is real-bounded and A2: X is closed ; ::_thesis: X is compact now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_X_holds_ ex_s2_being_Real_Sequence_st_ (_s2_is_subsequence_of_s1_&_s2_is_convergent_&_lim_s2_in_X_) let s1 be Real_Sequence; ::_thesis: ( rng s1 c= X implies ex s2 being Real_Sequence st ( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) ) assume A3: rng s1 c= X ; ::_thesis: ex s2 being Real_Sequence st ( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) A4: s1 is bounded_below proof consider p being real number such that A5: p is LowerBound of X by A1, XXREAL_2:def_9; A6: for q being real number st q in X holds p <= q by A5, XXREAL_2:def_2; take r = p - 1; :: according to SEQ_2:def_4 ::_thesis: for b1 being Element of NAT holds not s1 . b1 <= r A7: r + 1 = p - (1 - 1) ; A8: for t being real number st t in rng s1 holds r < t proof let t be real number ; ::_thesis: ( t in rng s1 implies r < t ) assume t in rng s1 ; ::_thesis: r < t then A9: p <= t by A3, A6; r < p by A7, XREAL_1:29; hence r < t by A9, XXREAL_0:2; ::_thesis: verum end; for n being Element of NAT holds r < s1 . n proof let n be Element of NAT ; ::_thesis: r < s1 . n n in NAT ; then n in dom s1 by FUNCT_2:def_1; then s1 . n in rng s1 by FUNCT_1:def_3; hence r < s1 . n by A8; ::_thesis: verum end; hence for b1 being Element of NAT holds not s1 . b1 <= r ; ::_thesis: verum end; s1 is bounded_above proof consider p being real number such that A10: p is UpperBound of X by A1, XXREAL_2:def_10; A11: for q being real number st q in X holds q <= p by A10, XXREAL_2:def_1; take r = p + 1; :: according to SEQ_2:def_3 ::_thesis: for b1 being Element of NAT holds not r <= s1 . b1 A12: for t being real number st t in rng s1 holds t < r proof let t be real number ; ::_thesis: ( t in rng s1 implies t < r ) assume t in rng s1 ; ::_thesis: t < r then A13: t <= p by A3, A11; p < r by XREAL_1:29; hence t < r by A13, XXREAL_0:2; ::_thesis: verum end; for n being Element of NAT holds s1 . n < r proof let n be Element of NAT ; ::_thesis: s1 . n < r n in NAT ; then n in dom s1 by FUNCT_2:def_1; then s1 . n in rng s1 by FUNCT_1:def_3; hence s1 . n < r by A12; ::_thesis: verum end; hence for b1 being Element of NAT holds not r <= s1 . b1 ; ::_thesis: verum end; then s1 is bounded by A4, SEQ_2:def_8; then consider s2 being Real_Sequence such that A14: s2 is subsequence of s1 and A15: s2 is convergent by SEQ_4:40; ex Nseq being increasing sequence of NAT st s2 = s1 * Nseq by A14, VALUED_0:def_17; then rng s2 c= rng s1 by RELAT_1:26; then rng s2 c= X by A3, XBOOLE_1:1; then lim s2 in X by A2, A15, Def4; hence ex s2 being Real_Sequence st ( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) by A14, A15; ::_thesis: verum end; hence X is compact by Def3; ::_thesis: verum end; theorem Th12: :: RCOMP_1:12 for X being Subset of REAL st X <> {} & X is closed & X is bounded_above holds upper_bound X in X proof let X be Subset of REAL; ::_thesis: ( X <> {} & X is closed & X is bounded_above implies upper_bound X in X ) assume that A1: X <> {} and A2: X is closed and A3: X is bounded_above and A4: not upper_bound X in X ; ::_thesis: contradiction set s1 = upper_bound X; defpred S1[ Element of NAT , Element of REAL ] means ex q being real number st ( q = $2 & q in X & (upper_bound X) - q < 1 / ($1 + 1) ); A5: for n being Element of NAT ex p being Element of REAL st S1[n,p] proof let n be Element of NAT ; ::_thesis: ex p being Element of REAL st S1[n,p] 0 < (n + 1) " ; then 0 < 1 / (n + 1) by XCMPLX_1:215; then consider t being real number such that A6: t in X and A7: (upper_bound X) - (1 / (n + 1)) < t by A1, A3, SEQ_4:def_1; take t ; ::_thesis: ( t is Element of REAL & S1[n,t] ) upper_bound X < t + (1 / (n + 1)) by A7, XREAL_1:19; then (upper_bound X) - t < 1 / (n + 1) by XREAL_1:19; hence ( t is Element of REAL & S1[n,t] ) by A6; ::_thesis: verum end; consider f being Function of NAT,REAL such that A8: for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch_3(A5); A9: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_f_._n_in_X_&_(upper_bound_X)_-_(f_._n)_<_1_/_(n_+_1)_) let n be Element of NAT ; ::_thesis: ( f . n in X & (upper_bound X) - (f . n) < 1 / (n + 1) ) ex q being real number st ( q = f . n & q in X & (upper_bound X) - q < 1 / (n + 1) ) by A8; hence ( f . n in X & (upper_bound X) - (f . n) < 1 / (n + 1) ) ; ::_thesis: verum end; A10: rng f c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in X ) assume x in rng f ; ::_thesis: x in X then consider y being set such that A11: y in dom f and A12: x = f . y by FUNCT_1:def_3; reconsider y = y as Element of NAT by A11, FUNCT_2:def_1; f . y in X by A9; hence x in X by A12; ::_thesis: verum end; A13: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ abs_((f_._m)_-_(upper_bound_X))_<_s let s be real number ; ::_thesis: ( 0 < s implies ex k being Element of NAT st for m being Element of NAT st k <= m holds abs ((f . m) - (upper_bound X)) < s ) assume A14: 0 < s ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds abs ((f . m) - (upper_bound X)) < s consider n being Element of NAT such that A15: s " < n by SEQ_4:3; take k = n; ::_thesis: for m being Element of NAT st k <= m holds abs ((f . m) - (upper_bound X)) < s let m be Element of NAT ; ::_thesis: ( k <= m implies abs ((f . m) - (upper_bound X)) < s ) assume k <= m ; ::_thesis: abs ((f . m) - (upper_bound X)) < s then k + 1 <= m + 1 by XREAL_1:6; then A16: 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:118; f . m in X by A9; then f . m <= upper_bound X by A3, SEQ_4:def_1; then A17: 0 <= (upper_bound X) - (f . m) by XREAL_1:48; (s ") + 0 < n + 1 by A15, XREAL_1:8; then 1 / (n + 1) < 1 / (s ") by A14, XREAL_1:76; then 1 / (n + 1) < s by XCMPLX_1:216; then 1 / (m + 1) < s by A16, XXREAL_0:2; then (upper_bound X) - (f . m) < s by A9, XXREAL_0:2; then abs (- ((f . m) - (upper_bound X))) < s by A17, ABSVALUE:def_1; hence abs ((f . m) - (upper_bound X)) < s by COMPLEX1:52; ::_thesis: verum end; then A18: f is convergent by SEQ_2:def_6; then lim f = upper_bound X by A13, SEQ_2:def_7; hence contradiction by A2, A4, A18, A10, Def4; ::_thesis: verum end; theorem Th13: :: RCOMP_1:13 for X being Subset of REAL st X <> {} & X is closed & X is bounded_below holds lower_bound X in X proof let X be Subset of REAL; ::_thesis: ( X <> {} & X is closed & X is bounded_below implies lower_bound X in X ) assume that A1: X <> {} and A2: X is closed and A3: X is bounded_below and A4: not lower_bound X in X ; ::_thesis: contradiction set i1 = lower_bound X; defpred S1[ Element of NAT , Element of REAL ] means ex q being real number st ( q = $2 & q in X & q - (lower_bound X) < 1 / ($1 + 1) ); A5: for n being Element of NAT ex p being Element of REAL st S1[n,p] proof let n be Element of NAT ; ::_thesis: ex p being Element of REAL st S1[n,p] 0 < (n + 1) " ; then 0 < 1 / (n + 1) by XCMPLX_1:215; then consider t being real number such that A6: t in X and A7: t < (lower_bound X) + (1 / (n + 1)) by A1, A3, SEQ_4:def_2; take t ; ::_thesis: ( t is Element of REAL & S1[n,t] ) t - (lower_bound X) < 1 / (n + 1) by A7, XREAL_1:19; hence ( t is Element of REAL & S1[n,t] ) by A6; ::_thesis: verum end; consider f being Function of NAT,REAL such that A8: for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch_3(A5); A9: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_f_._n_in_X_&_(f_._n)_-_(lower_bound_X)_<_1_/_(n_+_1)_) let n be Element of NAT ; ::_thesis: ( f . n in X & (f . n) - (lower_bound X) < 1 / (n + 1) ) ex q being real number st ( q = f . n & q in X & q - (lower_bound X) < 1 / (n + 1) ) by A8; hence ( f . n in X & (f . n) - (lower_bound X) < 1 / (n + 1) ) ; ::_thesis: verum end; A10: rng f c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in X ) assume x in rng f ; ::_thesis: x in X then consider y being set such that A11: y in dom f and A12: x = f . y by FUNCT_1:def_3; reconsider y = y as Element of NAT by A11, FUNCT_2:def_1; f . y in X by A9; hence x in X by A12; ::_thesis: verum end; A13: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ abs_((f_._m)_-_(lower_bound_X))_<_s let s be real number ; ::_thesis: ( 0 < s implies ex k being Element of NAT st for m being Element of NAT st k <= m holds abs ((f . m) - (lower_bound X)) < s ) assume A14: 0 < s ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds abs ((f . m) - (lower_bound X)) < s consider n being Element of NAT such that A15: s " < n by SEQ_4:3; take k = n; ::_thesis: for m being Element of NAT st k <= m holds abs ((f . m) - (lower_bound X)) < s let m be Element of NAT ; ::_thesis: ( k <= m implies abs ((f . m) - (lower_bound X)) < s ) assume k <= m ; ::_thesis: abs ((f . m) - (lower_bound X)) < s then k + 1 <= m + 1 by XREAL_1:6; then A16: 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:118; f . m in X by A9; then lower_bound X <= f . m by A3, SEQ_4:def_2; then A17: 0 <= (f . m) - (lower_bound X) by XREAL_1:48; (s ") + 0 < n + 1 by A15, XREAL_1:8; then 1 / (n + 1) < 1 / (s ") by A14, XREAL_1:76; then 1 / (n + 1) < s by XCMPLX_1:216; then 1 / (m + 1) < s by A16, XXREAL_0:2; then (f . m) - (lower_bound X) < s by A9, XXREAL_0:2; hence abs ((f . m) - (lower_bound X)) < s by A17, ABSVALUE:def_1; ::_thesis: verum end; then A18: f is convergent by SEQ_2:def_6; then lim f = lower_bound X by A13, SEQ_2:def_7; hence contradiction by A2, A4, A18, A10, Def4; ::_thesis: verum end; theorem :: RCOMP_1:14 for X being Subset of REAL st X <> {} & X is compact holds ( upper_bound X in X & lower_bound X in X ) proof let X be Subset of REAL; ::_thesis: ( X <> {} & X is compact implies ( upper_bound X in X & lower_bound X in X ) ) assume that A1: X <> {} and A2: X is compact ; ::_thesis: ( upper_bound X in X & lower_bound X in X ) ( X is real-bounded & X is closed ) by A2, Th10; hence ( upper_bound X in X & lower_bound X in X ) by A1, Th12, Th13; ::_thesis: verum end; theorem :: RCOMP_1:15 for X being Subset of REAL st X is compact & ( for g1, g2 being real number st g1 in X & g2 in X holds [.g1,g2.] c= X ) holds ex p, g being real number st X = [.p,g.] proof let X be Subset of REAL; ::_thesis: ( X is compact & ( for g1, g2 being real number st g1 in X & g2 in X holds [.g1,g2.] c= X ) implies ex p, g being real number st X = [.p,g.] ) assume that A1: X is compact and A2: for g1, g2 being real number st g1 in X & g2 in X holds [.g1,g2.] c= X ; ::_thesis: ex p, g being real number st X = [.p,g.] percases ( X = {} or X <> {} ) ; supposeA3: X = {} ; ::_thesis: ex p, g being real number st X = [.p,g.] take 1 ; ::_thesis: ex g being real number st X = [.1,g.] take 0 ; ::_thesis: X = [.1,0.] thus X = [.1,0.] by A3, XXREAL_1:29; ::_thesis: verum end; supposeA4: X <> {} ; ::_thesis: ex p, g being real number st X = [.p,g.] take p = lower_bound X; ::_thesis: ex g being real number st X = [.p,g.] take g = upper_bound X; ::_thesis: X = [.p,g.] A5: ( X is real-bounded & X is closed ) by A1, Th10; now__::_thesis:_for_r_being_Real_st_r_in_X_holds_ r_in_[.p,g.] let r be Real; ::_thesis: ( r in X implies r in [.p,g.] ) assume r in X ; ::_thesis: r in [.p,g.] then ( r <= g & p <= r ) by A5, SEQ_4:def_1, SEQ_4:def_2; hence r in [.p,g.] ; ::_thesis: verum end; then A6: X c= [.p,g.] by SUBSET_1:2; ( upper_bound X in X & lower_bound X in X ) by A4, A5, Th12, Th13; then [.p,g.] c= X by A2; hence X = [.p,g.] by A6, XBOOLE_0:def_10; ::_thesis: verum end; end; end; registration clusterV50() V51() V52() open for Element of K19(REAL); existence ex b1 being Subset of REAL st b1 is open proof take ].0,1.[ ; ::_thesis: ].0,1.[ is open thus ].0,1.[ is open ; ::_thesis: verum end; end; definition let r be real number ; mode Neighbourhood of r -> Subset of REAL means :Def6: :: RCOMP_1:def 6 ex g being real number st ( 0 < g & it = ].(r - g),(r + g).[ ); existence ex b1 being Subset of REAL ex g being real number st ( 0 < g & b1 = ].(r - g),(r + g).[ ) proof take ].(r - 1),(r + 1).[ ; ::_thesis: ex g being real number st ( 0 < g & ].(r - 1),(r + 1).[ = ].(r - g),(r + g).[ ) thus ex g being real number st ( 0 < g & ].(r - 1),(r + 1).[ = ].(r - g),(r + g).[ ) ; ::_thesis: verum end; end; :: deftheorem Def6 defines Neighbourhood RCOMP_1:def_6_:_ for r being real number for b2 being Subset of REAL holds ( b2 is Neighbourhood of r iff ex g being real number st ( 0 < g & b2 = ].(r - g),(r + g).[ ) ); registration let r be real number ; cluster -> open for Neighbourhood of r; coherence for b1 being Neighbourhood of r holds b1 is open proof let A be Neighbourhood of r; ::_thesis: A is open ex g being real number st ( 0 < g & A = ].(r - g),(r + g).[ ) by Def6; hence A is open ; ::_thesis: verum end; end; theorem :: RCOMP_1:16 for r being real number for N being Neighbourhood of r holds r in N proof let r be real number ; ::_thesis: for N being Neighbourhood of r holds r in N let N be Neighbourhood of r; ::_thesis: r in N ( ex g being real number st ( 0 < g & N = ].(r - g),(r + g).[ ) & abs (r - r) = 0 ) by Def6, ABSVALUE:2; hence r in N by Th1; ::_thesis: verum end; theorem :: RCOMP_1:17 for r being real number for N1, N2 being Neighbourhood of r ex N being Neighbourhood of r st ( N c= N1 & N c= N2 ) proof let r be real number ; ::_thesis: for N1, N2 being Neighbourhood of r ex N being Neighbourhood of r st ( N c= N1 & N c= N2 ) let N1, N2 be Neighbourhood of r; ::_thesis: ex N being Neighbourhood of r st ( N c= N1 & N c= N2 ) consider g1 being real number such that A1: 0 < g1 and A2: ].(r - g1),(r + g1).[ = N1 by Def6; consider g2 being real number such that A3: 0 < g2 and A4: ].(r - g2),(r + g2).[ = N2 by Def6; set g = min (g1,g2); 0 < min (g1,g2) by A1, A3, XXREAL_0:15; then reconsider N = ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ as Neighbourhood of r by Def6; take N ; ::_thesis: ( N c= N1 & N c= N2 ) A5: min (g1,g2) <= g1 by XXREAL_0:17; then A6: r + (min (g1,g2)) <= r + g1 by XREAL_1:7; - g1 <= - (min (g1,g2)) by A5, XREAL_1:24; then A7: r + (- g1) <= r + (- (min (g1,g2))) by XREAL_1:7; A8: min (g1,g2) <= g2 by XXREAL_0:17; then - g2 <= - (min (g1,g2)) by XREAL_1:24; then A9: r + (- g2) <= r + (- (min (g1,g2))) by XREAL_1:7; A10: r + (min (g1,g2)) <= r + g2 by A8, XREAL_1:7; now__::_thesis:_(_].(r_-_(min_(g1,g2))),(r_+_(min_(g1,g2))).[_c=_N1_&_].(r_-_(min_(g1,g2))),(r_+_(min_(g1,g2))).[_c=_N2_) percases ( g1 <= g2 or g2 <= g1 ) ; supposeA11: g1 <= g2 ; ::_thesis: ( ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N1 & ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N2 ) A12: now__::_thesis:_for_y_being_set_st_y_in_].(r_-_(min_(g1,g2))),(r_+_(min_(g1,g2))).[_holds_ y_in_].(r_-_g2),(r_+_g2).[ let y be set ; ::_thesis: ( y in ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ implies y in ].(r - g2),(r + g2).[ ) assume A13: y in ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ ; ::_thesis: y in ].(r - g2),(r + g2).[ then reconsider x1 = y as Real ; ex p2 being Real st ( y = p2 & r - (min (g1,g2)) < p2 & p2 < r + (min (g1,g2)) ) by A13; then ( x1 < r + g2 & r - g2 < x1 ) by A10, A9, XXREAL_0:2; hence y in ].(r - g2),(r + g2).[ ; ::_thesis: verum end; g1 = min (g1,g2) by A11, XXREAL_0:def_9; hence ( ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N1 & ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N2 ) by A2, A4, A12, TARSKI:def_3; ::_thesis: verum end; supposeA14: g2 <= g1 ; ::_thesis: ( ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N1 & ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N2 ) A15: now__::_thesis:_for_y_being_set_st_y_in_].(r_-_(min_(g1,g2))),(r_+_(min_(g1,g2))).[_holds_ y_in_].(r_-_g1),(r_+_g1).[ let y be set ; ::_thesis: ( y in ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ implies y in ].(r - g1),(r + g1).[ ) assume A16: y in ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ ; ::_thesis: y in ].(r - g1),(r + g1).[ then reconsider x1 = y as Real ; ex p2 being Real st ( y = p2 & r - (min (g1,g2)) < p2 & p2 < r + (min (g1,g2)) ) by A16; then ( x1 < r + g1 & r - g1 < x1 ) by A6, A7, XXREAL_0:2; hence y in ].(r - g1),(r + g1).[ ; ::_thesis: verum end; g2 = min (g1,g2) by A14, XXREAL_0:def_9; hence ( ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N1 & ].(r - (min (g1,g2))),(r + (min (g1,g2))).[ c= N2 ) by A2, A4, A15, TARSKI:def_3; ::_thesis: verum end; end; end; hence ( N c= N1 & N c= N2 ) ; ::_thesis: verum end; theorem Th18: :: RCOMP_1:18 for X being open Subset of REAL for r being real number st r in X holds ex N being Neighbourhood of r st N c= X proof let X be open Subset of REAL; ::_thesis: for r being real number st r in X holds ex N being Neighbourhood of r st N c= X let r be real number ; ::_thesis: ( r in X implies ex N being Neighbourhood of r st N c= X ) assume that A1: r in X and A2: for N being Neighbourhood of r holds not N c= X ; ::_thesis: contradiction defpred S1[ Element of NAT , real number ] means ( $2 in ].(r - (1 / ($1 + 1))),(r + (1 / ($1 + 1))).[ & $2 in X ` ); A3: now__::_thesis:_for_N_being_Neighbourhood_of_r_ex_s_being_Real_st_ (_s_in_N_&_s_in_X_`_) let N be Neighbourhood of r; ::_thesis: ex s being Real st ( s in N & s in X ` ) consider g being real number such that 0 < g and A4: N = ].(r - g),(r + g).[ by Def6; not N c= X by A2; then consider x being set such that A5: x in N and A6: not x in X by TARSKI:def_3; consider s being Real such that A7: x = s and r - g < s and s < r + g by A5, A4; take s = s; ::_thesis: ( s in N & s in X ` ) thus s in N by A5, A7; ::_thesis: s in X ` thus s in X ` by A6, A7, XBOOLE_0:def_5; ::_thesis: verum end; A8: for n being Element of NAT ex s being Real st S1[n,s] proof let n be Element of NAT ; ::_thesis: ex s being Real st S1[n,s] 0 < 1 * ((n + 1) ") ; then 0 < 1 / (n + 1) by XCMPLX_0:def_9; then reconsider N = ].(r - (1 / (n + 1))),(r + (1 / (n + 1))).[ as Neighbourhood of r by Def6; ex s being Real st ( s in N & s in X ` ) by A3; hence ex s being Real st S1[n,s] ; ::_thesis: verum end; consider s3 being Real_Sequence such that A9: for n being Element of NAT holds S1[n,s3 . n] from FUNCT_2:sch_3(A8); deffunc H1( Element of NAT ) -> Element of REAL = r + (1 / ($1 + 1)); deffunc H2( Element of NAT ) -> Element of REAL = r - (1 / ($1 + 1)); consider s1 being Real_Sequence such that A10: for n being Element of NAT holds s1 . n = H2(n) from SEQ_1:sch_1(); consider s2 being Real_Sequence such that A11: for n being Element of NAT holds s2 . n = H1(n) from SEQ_1:sch_1(); A12: for n being Element of NAT holds ( s1 . n <= s3 . n & s3 . n <= s2 . n ) proof let n be Element of NAT ; ::_thesis: ( s1 . n <= s3 . n & s3 . n <= s2 . n ) s3 . n in ].(r - (1 / (n + 1))),(r + (1 / (n + 1))).[ by A9; then A13: ex s being Real st ( s = s3 . n & r - (1 / (n + 1)) < s & s < r + (1 / (n + 1)) ) ; hence s1 . n <= s3 . n by A10; ::_thesis: s3 . n <= s2 . n thus s3 . n <= s2 . n by A11, A13; ::_thesis: verum end; A14: rng s3 c= X ` proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng s3 or x in X ` ) assume x in rng s3 ; ::_thesis: x in X ` then consider y being set such that A15: y in dom s3 and A16: s3 . y = x by FUNCT_1:def_3; reconsider y = y as Element of NAT by A15, FUNCT_2:def_1; s3 . y in X ` by A9; hence x in X ` by A16; ::_thesis: verum end; A17: X ` is closed by Def5; A18: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ abs_((s2_._m)_-_r)_<_s let s be real number ; ::_thesis: ( 0 < s implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((s2 . m) - r) < s ) assume A19: 0 < s ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((s2 . m) - r) < s consider n being Element of NAT such that A20: s " < n by SEQ_4:3; take n = n; ::_thesis: for m being Element of NAT st n <= m holds abs ((s2 . m) - r) < s let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((s2 . m) - r) < s ) assume n <= m ; ::_thesis: abs ((s2 . m) - r) < s then n + 1 <= m + 1 by XREAL_1:6; then A21: 1 / (m + 1) <= 1 / (n + 1) by XREAL_1:118; (s ") + 0 < n + 1 by A20, XREAL_1:8; then 1 / (n + 1) < 1 / (s ") by A19, XREAL_1:76; then A22: 1 / (n + 1) < s by XCMPLX_1:216; abs ((s2 . m) - r) = abs ((r + (1 / (m + 1))) - r) by A11 .= 1 / (m + 1) by ABSVALUE:def_1 ; hence abs ((s2 . m) - r) < s by A22, A21, XXREAL_0:2; ::_thesis: verum end; then A23: s2 is convergent by SEQ_2:def_6; then A24: lim s2 = r by A18, SEQ_2:def_7; A25: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ abs_((s1_._m)_-_r)_<_s let s be real number ; ::_thesis: ( 0 < s implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((s1 . m) - r) < s ) assume A26: 0 < s ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((s1 . m) - r) < s consider n being Element of NAT such that A27: s " < n by SEQ_4:3; take n = n; ::_thesis: for m being Element of NAT st n <= m holds abs ((s1 . m) - r) < s let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((s1 . m) - r) < s ) assume n <= m ; ::_thesis: abs ((s1 . m) - r) < s then n + 1 <= m + 1 by XREAL_1:6; then A28: 1 / (m + 1) <= 1 / (n + 1) by XREAL_1:118; (s ") + 0 < n + 1 by A27, XREAL_1:8; then 1 / (n + 1) < 1 / (s ") by A26, XREAL_1:76; then A29: 1 / (n + 1) < s by XCMPLX_1:216; abs ((s1 . m) - r) = abs ((r - (1 / (m + 1))) - r) by A10 .= abs (- (1 / (m + 1))) .= abs (1 / (m + 1)) by COMPLEX1:52 .= 1 / (m + 1) by ABSVALUE:def_1 ; hence abs ((s1 . m) - r) < s by A29, A28, XXREAL_0:2; ::_thesis: verum end; then A30: s1 is convergent by SEQ_2:def_6; then lim s1 = r by A25, SEQ_2:def_7; then ( s3 is convergent & lim s3 = r ) by A30, A23, A24, A12, SEQ_2:19, SEQ_2:20; then r in X ` by A14, A17, Def4; hence contradiction by A1, XBOOLE_0:def_5; ::_thesis: verum end; theorem :: RCOMP_1:19 for X being open Subset of REAL for r being real number st r in X holds ex g being real number st ( 0 < g & ].(r - g),(r + g).[ c= X ) proof let X be open Subset of REAL; ::_thesis: for r being real number st r in X holds ex g being real number st ( 0 < g & ].(r - g),(r + g).[ c= X ) let r be real number ; ::_thesis: ( r in X implies ex g being real number st ( 0 < g & ].(r - g),(r + g).[ c= X ) ) assume r in X ; ::_thesis: ex g being real number st ( 0 < g & ].(r - g),(r + g).[ c= X ) then consider N being Neighbourhood of r such that A1: N c= X by Th18; consider g being real number such that A2: ( 0 < g & N = ].(r - g),(r + g).[ ) by Def6; take g ; ::_thesis: ( 0 < g & ].(r - g),(r + g).[ c= X ) thus ( 0 < g & ].(r - g),(r + g).[ c= X ) by A1, A2; ::_thesis: verum end; theorem :: RCOMP_1:20 for X being Subset of REAL st ( for r being real number st r in X holds ex N being Neighbourhood of r st N c= X ) holds X is open proof let X be Subset of REAL; ::_thesis: ( ( for r being real number st r in X holds ex N being Neighbourhood of r st N c= X ) implies X is open ) assume that A1: for r being real number st r in X holds ex N being Neighbourhood of r st N c= X and A2: not X is open ; ::_thesis: contradiction not X ` is closed by A2, Def5; then consider s1 being Real_Sequence such that A3: rng s1 c= X ` and A4: s1 is convergent and A5: not lim s1 in X ` by Def4; consider N being Neighbourhood of lim s1 such that A6: N c= X by A1, A5, SUBSET_1:29; consider g being real number such that A7: 0 < g and A8: ].((lim s1) - g),((lim s1) + g).[ = N by Def6; consider n being Element of NAT such that A9: for m being Element of NAT st n <= m holds abs ((s1 . m) - (lim s1)) < g by A4, A7, SEQ_2:def_7; n in NAT ; then n in dom s1 by FUNCT_2:def_1; then A10: s1 . n in rng s1 by FUNCT_1:def_3; A11: abs ((s1 . n) - (lim s1)) < g by A9; then (s1 . n) - (lim s1) < g by SEQ_2:1; then A12: s1 . n < (lim s1) + g by XREAL_1:19; - g < (s1 . n) - (lim s1) by A11, SEQ_2:1; then (lim s1) + (- g) < (lim s1) + ((s1 . n) - (lim s1)) by XREAL_1:6; then s1 . n in { s where s is Real : ( (lim s1) - g < s & s < (lim s1) + g ) } by A12; hence contradiction by A3, A6, A8, A10, XBOOLE_0:def_5; ::_thesis: verum end; theorem Th21: :: RCOMP_1:21 for X being Subset of REAL st X is open & X is bounded_above holds not upper_bound X in X proof let X be Subset of REAL; ::_thesis: ( X is open & X is bounded_above implies not upper_bound X in X ) assume that A1: X is open and A2: X is bounded_above ; ::_thesis: not upper_bound X in X assume upper_bound X in X ; ::_thesis: contradiction then consider N being Neighbourhood of upper_bound X such that A3: N c= X by A1, Th18; consider t being real number such that A4: t > 0 and A5: N = ].((upper_bound X) - t),((upper_bound X) + t).[ by Def6; A6: (upper_bound X) + (t / 2) > upper_bound X by A4, XREAL_1:29, XREAL_1:215; A7: ((upper_bound X) + (t / 2)) + (t / 2) > (upper_bound X) + (t / 2) by A4, XREAL_1:29, XREAL_1:215; (upper_bound X) - t < upper_bound X by A4, XREAL_1:44; then (upper_bound X) - t < (upper_bound X) + (t / 2) by A6, XXREAL_0:2; then (upper_bound X) + (t / 2) in { s where s is Real : ( (upper_bound X) - t < s & s < (upper_bound X) + t ) } by A7; hence contradiction by A2, A3, A5, A6, SEQ_4:def_1; ::_thesis: verum end; theorem Th22: :: RCOMP_1:22 for X being Subset of REAL st X is open & X is bounded_below holds not lower_bound X in X proof let X be Subset of REAL; ::_thesis: ( X is open & X is bounded_below implies not lower_bound X in X ) assume that A1: X is open and A2: X is bounded_below ; ::_thesis: not lower_bound X in X assume lower_bound X in X ; ::_thesis: contradiction then consider N being Neighbourhood of lower_bound X such that A3: N c= X by A1, Th18; consider t being real number such that A4: t > 0 and A5: N = ].((lower_bound X) - t),((lower_bound X) + t).[ by Def6; A6: (lower_bound X) - (t / 2) < lower_bound X by A4, XREAL_1:44, XREAL_1:215; A7: ((lower_bound X) - (t / 2)) - (t / 2) < (lower_bound X) - (t / 2) by A4, XREAL_1:44, XREAL_1:215; lower_bound X < (lower_bound X) + t by A4, XREAL_1:29; then (lower_bound X) - (t / 2) < (lower_bound X) + t by A6, XXREAL_0:2; then (lower_bound X) - (t / 2) in { s where s is Real : ( (lower_bound X) - t < s & s < (lower_bound X) + t ) } by A7; hence contradiction by A2, A3, A5, A6, SEQ_4:def_2; ::_thesis: verum end; theorem :: RCOMP_1:23 for X being Subset of REAL st X is open & X is real-bounded & ( for g1, g2 being real number st g1 in X & g2 in X holds [.g1,g2.] c= X ) holds ex p, g being real number st X = ].p,g.[ proof let X be Subset of REAL; ::_thesis: ( X is open & X is real-bounded & ( for g1, g2 being real number st g1 in X & g2 in X holds [.g1,g2.] c= X ) implies ex p, g being real number st X = ].p,g.[ ) assume that A1: X is open and A2: X is real-bounded and A3: for g1, g2 being real number st g1 in X & g2 in X holds [.g1,g2.] c= X ; ::_thesis: ex p, g being real number st X = ].p,g.[ percases ( X = {} or X <> {} ) ; supposeA4: X = {} ; ::_thesis: ex p, g being real number st X = ].p,g.[ take 1 ; ::_thesis: ex g being real number st X = ].1,g.[ take 0 ; ::_thesis: X = ].1,0.[ thus X = ].1,0.[ by A4, XXREAL_1:28; ::_thesis: verum end; supposeA5: X <> {} ; ::_thesis: ex p, g being real number st X = ].p,g.[ take p = lower_bound X; ::_thesis: ex g being real number st X = ].p,g.[ take g = upper_bound X; ::_thesis: X = ].p,g.[ now__::_thesis:_for_r_being_Real_holds_ (_(_r_in_X_implies_r_in_].p,g.[_)_&_(_r_in_].p,g.[_implies_r_in_X_)_) let r be Real; ::_thesis: ( ( r in X implies r in ].p,g.[ ) & ( r in ].p,g.[ implies r in X ) ) thus ( r in X implies r in ].p,g.[ ) ::_thesis: ( r in ].p,g.[ implies r in X ) proof assume A6: r in X ; ::_thesis: r in ].p,g.[ then ( p <> r & p <= r ) by A1, A2, Th22, SEQ_4:def_2; then A7: p < r by XXREAL_0:1; ( g <> r & r <= g ) by A1, A2, A6, Th21, SEQ_4:def_1; then r < g by XXREAL_0:1; hence r in ].p,g.[ by A7; ::_thesis: verum end; assume r in ].p,g.[ ; ::_thesis: r in X then A8: ex s being Real st ( s = r & p < s & s < g ) ; then g - r > 0 by XREAL_1:50; then consider g2 being real number such that A9: ( g2 in X & g - (g - r) < g2 ) by A2, A5, SEQ_4:def_1; r - p > 0 by A8, XREAL_1:50; then consider g1 being real number such that A10: ( g1 in X & g1 < p + (r - p) ) by A2, A5, SEQ_4:def_2; reconsider g1 = g1, g2 = g2 as Real by XREAL_0:def_1; ( r in { s where s is Real : ( g1 <= s & s <= g2 ) } & [.g1,g2.] c= X ) by A3, A9, A10; hence r in X ; ::_thesis: verum end; hence X = ].p,g.[ by SUBSET_1:3; ::_thesis: verum end; end; end; definition let g be real number ; let s be ext-real number ; :: original: [. redefine func[.g,s.[ -> Subset of REAL equals :: RCOMP_1:def 7 { r where r is Real : ( g <= r & r < s ) } ; coherence [.g,s.[ is Subset of REAL proof now__::_thesis:_for_e_being_set_st_e_in_[.g,s.[_holds_ e_in_REAL let e be set ; ::_thesis: ( e in [.g,s.[ implies e in REAL ) assume e in [.g,s.[ ; ::_thesis: e in REAL then A1: ex r being Element of ExtREAL st ( e = r & g <= r & r < s ) ; g in REAL by XREAL_0:def_1; hence e in REAL by A1, XXREAL_0:46; ::_thesis: verum end; hence [.g,s.[ is Subset of REAL by TARSKI:def_3; ::_thesis: verum end; compatibility for b1 being Subset of REAL holds ( b1 = [.g,s.[ iff b1 = { r where r is Real : ( g <= r & r < s ) } ) proof set Y = { r where r is Real : ( g <= r & r < s ) } ; let X be Subset of REAL; ::_thesis: ( X = [.g,s.[ iff X = { r where r is Real : ( g <= r & r < s ) } ) A2: [.g,s.[ c= { r where r is Real : ( g <= r & r < s ) } proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in [.g,s.[ or e in { r where r is Real : ( g <= r & r < s ) } ) assume e in [.g,s.[ ; ::_thesis: e in { r where r is Real : ( g <= r & r < s ) } then consider r being Element of ExtREAL such that A3: e = r and A4: ( g <= r & r < s ) ; g in REAL by XREAL_0:def_1; then r in REAL by A4, XXREAL_0:46; hence e in { r where r is Real : ( g <= r & r < s ) } by A3, A4; ::_thesis: verum end; { r where r is Real : ( g <= r & r < s ) } c= [.g,s.[ proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { r where r is Real : ( g <= r & r < s ) } or e in [.g,s.[ ) assume e in { r where r is Real : ( g <= r & r < s ) } ; ::_thesis: e in [.g,s.[ then consider r being Element of REAL such that A5: ( e = r & g <= r & r < s ) ; r in REAL ; hence e in [.g,s.[ by A5, NUMBERS:31; ::_thesis: verum end; hence ( X = [.g,s.[ iff X = { r where r is Real : ( g <= r & r < s ) } ) by A2, XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem defines [. RCOMP_1:def_7_:_ for g being real number for s being ext-real number holds [.g,s.[ = { r where r is Real : ( g <= r & r < s ) } ; definition let g be ext-real number ; let s be real number ; :: original: ]. redefine func].g,s.] -> Subset of REAL equals :: RCOMP_1:def 8 { r where r is Real : ( g < r & r <= s ) } ; coherence ].g,s.] is Subset of REAL proof now__::_thesis:_for_e_being_set_st_e_in_].g,s.]_holds_ e_in_REAL let e be set ; ::_thesis: ( e in ].g,s.] implies e in REAL ) assume e in ].g,s.] ; ::_thesis: e in REAL then A1: ex r being Element of ExtREAL st ( e = r & g < r & r <= s ) ; s in REAL by XREAL_0:def_1; hence e in REAL by A1, XXREAL_0:47; ::_thesis: verum end; hence ].g,s.] is Subset of REAL by TARSKI:def_3; ::_thesis: verum end; compatibility for b1 being Subset of REAL holds ( b1 = ].g,s.] iff b1 = { r where r is Real : ( g < r & r <= s ) } ) proof set Y = { r where r is Real : ( g < r & r <= s ) } ; let X be Subset of REAL; ::_thesis: ( X = ].g,s.] iff X = { r where r is Real : ( g < r & r <= s ) } ) A2: ].g,s.] c= { r where r is Real : ( g < r & r <= s ) } proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in ].g,s.] or e in { r where r is Real : ( g < r & r <= s ) } ) assume e in ].g,s.] ; ::_thesis: e in { r where r is Real : ( g < r & r <= s ) } then consider r being Element of ExtREAL such that A3: e = r and A4: ( g < r & r <= s ) ; s in REAL by XREAL_0:def_1; then r in REAL by A4, XXREAL_0:47; hence e in { r where r is Real : ( g < r & r <= s ) } by A3, A4; ::_thesis: verum end; { r where r is Real : ( g < r & r <= s ) } c= ].g,s.] proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { r where r is Real : ( g < r & r <= s ) } or e in ].g,s.] ) assume e in { r where r is Real : ( g < r & r <= s ) } ; ::_thesis: e in ].g,s.] then consider r being Element of REAL such that A5: ( e = r & g < r & r <= s ) ; r in REAL ; hence e in ].g,s.] by A5, NUMBERS:31; ::_thesis: verum end; hence ( X = ].g,s.] iff X = { r where r is Real : ( g < r & r <= s ) } ) by A2, XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem defines ]. RCOMP_1:def_8_:_ for g being ext-real number for s being real number holds ].g,s.] = { r where r is Real : ( g < r & r <= s ) } ;