let b be Real; :: thesis: Intersection (ext_half_open_sets b) = [.b,+infty.]

for c being object holds

( c in Intersection (ext_half_open_sets b) iff c in [.b,+infty.] )

for c being object holds

( c in Intersection (ext_half_open_sets b) iff c in [.b,+infty.] )

proof

hence
Intersection (ext_half_open_sets b) = [.b,+infty.]
; :: thesis: verum
let c be object ; :: thesis: ( c in Intersection (ext_half_open_sets b) iff c in [.b,+infty.] )

A1: ( not c in [.b,+infty.] implies not c in Intersection (ext_half_open_sets b) )

end;A1: ( not c in [.b,+infty.] implies not c in Intersection (ext_half_open_sets b) )

proof

( c in [.b,+infty.] implies c in Intersection (ext_half_open_sets b) )
assume A2:
not c in [.b,+infty.]
; :: thesis: not c in Intersection (ext_half_open_sets b)

end;per cases
( not c in ExtREAL or ( c in ExtREAL & not c in [.b,+infty.] ) )
by A2;

end;

suppose
( c in ExtREAL & not c in [.b,+infty.] )
; :: thesis: not c in Intersection (ext_half_open_sets b)

then reconsider c = c as ExtReal ;

W: c <> +infty

end;W: c <> +infty

proof

reconsider b = b as Element of REAL by XREAL_0:def 1;

not b > +infty by XXREAL_0:9;

hence c <> +infty by A2, XXREAL_1:1; :: thesis: verum

end;not b > +infty by XXREAL_0:9;

hence c <> +infty by A2, XXREAL_1:1; :: thesis: verum

per cases
( c = -infty or c in REAL )
by W, XXREAL_0:14;

end;

suppose S1:
c = -infty
; :: thesis: not c in Intersection (ext_half_open_sets b)

not c in Intersection (ext_half_open_sets b)

end;proof

hence
not c in Intersection (ext_half_open_sets b)
; :: thesis: verum
( c in ].(b - 1),+infty.] iff ( c > b - 1 & c <= +infty ) )
by XXREAL_1:2;

then not c in (ext_half_open_sets b) . 0 by Def300, S1, XXREAL_0:5;

hence not c in Intersection (ext_half_open_sets b) by PROB_1:13; :: thesis: verum

end;then not c in (ext_half_open_sets b) . 0 by Def300, S1, XXREAL_0:5;

hence not c in Intersection (ext_half_open_sets b) by PROB_1:13; :: thesis: verum

suppose
c in REAL
; :: thesis: not c in Intersection (ext_half_open_sets b)

then reconsider c = c as Element of REAL ;

not for n being Element of NAT holds c in (ext_half_open_sets b) . n

end;not for n being Element of NAT holds c in (ext_half_open_sets b) . n

proof

hence
not c in Intersection (ext_half_open_sets b)
by PROB_1:13; :: thesis: verum
set bc = b - c;

KK: b - c > 0

W1: ( 1 / n < b - c & n > 0 ) by KK, PP;

reconsider spec = 1 / n as Real ;

F0: c <= b - (1 / n) by XREAL_1:11, W1;

n < n + 1 by NAT_1:13;

then (n + 1) " < n " by W1, XREAL_1:88;

then 1 / (n + 1) < n " by XCMPLX_1:215;

then 1 / (n + 1) < 1 / n by XCMPLX_1:215;

then f: b - (1 / n) < b - (1 / (n + 1)) by XREAL_1:10;

f1: not c in ].(b - (1 / (n + 1))),+infty.]

end;KK: b - c > 0

proof

consider n being Nat such that
( c >= b implies c in [.b,+infty.] )

then (- 1) * (c + (- b)) > 0 ;

hence b - c > 0 ; :: thesis: verum

end;proof

then
c - b < 0
by XREAL_1:49, A2;
assume ASS0:
c >= b
; :: thesis: c in [.b,+infty.]

reconsider c = c as Element of ExtREAL by NUMBERS:31;

( b <= c & c <= +infty ) by XXREAL_0:3, ASS0;

then c in { a where a is Element of ExtREAL : ( b <= a & a <= +infty ) } ;

hence c in [.b,+infty.] by XXREAL_1:def 1; :: thesis: verum

end;reconsider c = c as Element of ExtREAL by NUMBERS:31;

( b <= c & c <= +infty ) by XXREAL_0:3, ASS0;

then c in { a where a is Element of ExtREAL : ( b <= a & a <= +infty ) } ;

hence c in [.b,+infty.] by XXREAL_1:def 1; :: thesis: verum

then (- 1) * (c + (- b)) > 0 ;

hence b - c > 0 ; :: thesis: verum

W1: ( 1 / n < b - c & n > 0 ) by KK, PP;

reconsider spec = 1 / n as Real ;

F0: c <= b - (1 / n) by XREAL_1:11, W1;

n < n + 1 by NAT_1:13;

then (n + 1) " < n " by W1, XREAL_1:88;

then 1 / (n + 1) < n " by XCMPLX_1:215;

then 1 / (n + 1) < 1 / n by XCMPLX_1:215;

then f: b - (1 / n) < b - (1 / (n + 1)) by XREAL_1:10;

f1: not c in ].(b - (1 / (n + 1))),+infty.]

proof

not for n being Element of NAT holds c in (ext_half_open_sets b) . n
( c in ].(b - (1 / (n + 1))),+infty.] implies c >= b - (1 / (n + 1)) )

end;proof

hence
not c in ].(b - (1 / (n + 1))),+infty.]
by f, F0, XXREAL_0:2; :: thesis: verum
assume
c in ].(b - (1 / (n + 1))),+infty.]
; :: thesis: c >= b - (1 / (n + 1))

then c in { e where e is Element of ExtREAL : ( b - (1 / (n + 1)) < e & e <= +infty ) } by XXREAL_1:def 3;

then consider e being Element of ExtREAL such that

E1: ( e = c & b - (1 / (n + 1)) < e & e <= +infty ) ;

thus c >= b - (1 / (n + 1)) by E1; :: thesis: verum

end;then c in { e where e is Element of ExtREAL : ( b - (1 / (n + 1)) < e & e <= +infty ) } by XXREAL_1:def 3;

then consider e being Element of ExtREAL such that

E1: ( e = c & b - (1 / (n + 1)) < e & e <= +infty ) ;

thus c >= b - (1 / (n + 1)) by E1; :: thesis: verum

proof

hence
not for n being Element of NAT holds c in (ext_half_open_sets b) . n
; :: thesis: verum
take nn = n + 1; :: thesis: ( nn is Element of NAT & not c in (ext_half_open_sets b) . nn )

thus ( nn is Element of NAT & not c in (ext_half_open_sets b) . nn ) by ORDINAL1:def 12, f1, Def300; :: thesis: verum

end;thus ( nn is Element of NAT & not c in (ext_half_open_sets b) . nn ) by ORDINAL1:def 12, f1, Def300; :: thesis: verum

proof

hence
( c in Intersection (ext_half_open_sets b) iff c in [.b,+infty.] )
by A1; :: thesis: verum
assume A12:
c in [.b,+infty.]
; :: thesis: c in Intersection (ext_half_open_sets b)

for n being Nat holds c in (ext_half_open_sets b) . n

end;for n being Nat holds c in (ext_half_open_sets b) . n

proof

hence
c in Intersection (ext_half_open_sets b)
by PROB_1:13; :: thesis: verum
let n be Nat; :: thesis: c in (ext_half_open_sets b) . n

end;per cases
( n = 0 or n > 0 )
;

end;

suppose
n = 0
; :: thesis: c in (ext_half_open_sets b) . n

then s2:
(ext_half_open_sets b) . n = ].(b - 1),+infty.]
by Def300;

[.b,+infty.] c= ].(b - 1),+infty.] by XX;

hence c in (ext_half_open_sets b) . n by A12, s2; :: thesis: verum

end;[.b,+infty.] c= ].(b - 1),+infty.] by XX;

hence c in (ext_half_open_sets b) . n by A12, s2; :: thesis: verum

suppose S1:
n > 0
; :: thesis: c in (ext_half_open_sets b) . n

then reconsider nminus1 = n - 1 as Nat by NAT_1:20;

s2: (ext_half_open_sets b) . (nminus1 + 1) = ].(b - (1 / (nminus1 + 1))),+infty.] by Def300;

[.b,+infty.] c= ].(b - (1 / n)),+infty.] by S1, Lemma2;

hence c in (ext_half_open_sets b) . n by A12, s2; :: thesis: verum

end;s2: (ext_half_open_sets b) . (nminus1 + 1) = ].(b - (1 / (nminus1 + 1))),+infty.] by Def300;

[.b,+infty.] c= ].(b - (1 / n)),+infty.] by S1, Lemma2;

hence c in (ext_half_open_sets b) . n by A12, s2; :: thesis: verum