let b be Real; :: thesis:
for c being object holds
( c in Intersection (ext_half_open_sets b) iff c in [.b,+infty.] )

proof

let c be object ; :: thesis:
A1: ( not c in [.b,+infty.] implies not c in Intersection (ext_half_open_sets b) )

proof

assume A2: not c in [.b,+infty.] ; :: thesis:

per cases by A2;

suppose not c in ExtREAL ; :: thesis:

hence not c in Intersection (ext_half_open_sets b) ; :: thesis:

end;

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

then reconsider c = c as ExtReal ;
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:

end;

per cases by W, XXREAL_0:14;

suppose S1: c = -infty ; :: thesis:

not c in Intersection (ext_half_open_sets b)

proof

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

end;

hence not c in Intersection (ext_half_open_sets b) ; :: thesis:

end;

suppose c in REAL ; :: thesis:

then reconsider c = c as Element of REAL ;
not for n being Element of NAT holds c in (ext_half_open_sets b) . n

proof

set bc = b - c;
KK: b - c > 0

proof

( c >= b implies c in [.b,+infty.] )

proof

assume ASS0: c >= b ; :: thesis:
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:

end;

then c - b < 0 by XREAL_1:49, A2;
then (- 1) * (c + (- b)) > 0 ;
hence b - c > 0 ; :: thesis:

end;

consider n being Nat such that
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

( c in ].(b - (1 / (n + 1))),+infty.] implies c >= b - (1 / (n + 1)) )

proof

assume c in ].(b - (1 / (n + 1))),+infty.] ; :: thesis:
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:

end;

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

end;

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

proof

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

end;

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

end;

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

end;

end;

end;

end;

end;

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

proof

assume A12: c in [.b,+infty.] ; :: thesis:
for n being Nat holds c in (ext_half_open_sets b) . n

proof

let n be Nat; :: thesis:

per cases ;

suppose n = 0 ; :: thesis:

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:

end;

suppose S1: n > 0 ; :: thesis:

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:

end;

end;

end;

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

end;

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

end;

hence Intersection (ext_half_open_sets b) = [.b,+infty.] ; :: thesis: