for c being object holds

( c in Intersection (ext_left_closed_sets 0) iff c in {+infty} )

( c in Intersection (ext_left_closed_sets 0) iff c in {+infty} )

proof

hence
Intersection (ext_left_closed_sets 0) = {+infty}
; :: thesis: verum
let c be object ; :: thesis: ( c in Intersection (ext_left_closed_sets 0) iff c in {+infty} )

thus ( c in Intersection (ext_left_closed_sets 0) implies c in {+infty} ) :: thesis: ( c in {+infty} implies c in Intersection (ext_left_closed_sets 0) )

for n being Nat holds c in (ext_left_closed_sets 0) . n

end;thus ( c in Intersection (ext_left_closed_sets 0) implies c in {+infty} ) :: thesis: ( c in {+infty} implies c in Intersection (ext_left_closed_sets 0) )

proof

assume A12:
c in {+infty}
; :: thesis: c in Intersection (ext_left_closed_sets 0)
assume Y:
c in Intersection (ext_left_closed_sets 0)
; :: thesis: c in {+infty}

assume not c in {+infty} ; :: thesis: contradiction

then WW: c <> +infty by TARSKI:def 1;

reconsider c = c as Element of ExtREAL by Y;

end;assume not c in {+infty} ; :: thesis: contradiction

then WW: c <> +infty by TARSKI:def 1;

reconsider c = c as Element of ExtREAL by Y;

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

end;

suppose
c = -infty
; :: thesis: contradiction

then
not c in [.(0 + 0),+infty.]
by XXREAL_1:1;

then not c in (ext_left_closed_sets 0) . 0 by Def4000;

hence contradiction by Y, PROB_1:13; :: thesis: verum

end;then not c in (ext_left_closed_sets 0) . 0 by Def4000;

hence contradiction by Y, PROB_1:13; :: thesis: verum

suppose
c in REAL
; :: thesis: contradiction

then reconsider c = c as Element of REAL ;

end;per cases
( c < 0 or c >= 0 )
;

end;

suppose
c < 0
; :: thesis: contradiction

then
not c in [.(0 + 1),+infty.]
by XXREAL_1:1;

then not c in (ext_left_closed_sets 0) . 1 by Def4000;

hence contradiction by Y, PROB_1:13; :: thesis: verum

end;then not c in (ext_left_closed_sets 0) . 1 by Def4000;

hence contradiction by Y, PROB_1:13; :: thesis: verum

suppose S1:
c >= 0
; :: thesis: contradiction

set finerg = [\(c + (2 * 1))/];

WQ1: (c + (2 * 1)) - 1 < [\(c + (2 * 1))/] by INT_1:def 6;

WQ: [\(c + (2 * 1))/] > 0 [\(c + (2 * 1))/] is Nat

W0: (c + (2 * 1)) - 1 < finerg by INT_1:def 6;

(c + (2 * 1)) - 1 = c + 1 ;

then W1: c < (c + (2 * 1)) - 1 by XREAL_1:29;

W2: finerg < 0 + (finerg + 1) by XREAL_1:29;

c < finerg by W0, W1, XXREAL_0:2;

then c < 0 + (finerg + 1) by W2, XXREAL_0:2;

then not c in [.(0 + (finerg + 1)),+infty.] by XXREAL_1:1;

then not c in (ext_left_closed_sets 0) . (finerg + 1) by Def4000;

hence contradiction by Y, PROB_1:13; :: thesis: verum

end;WQ1: (c + (2 * 1)) - 1 < [\(c + (2 * 1))/] by INT_1:def 6;

WQ: [\(c + (2 * 1))/] > 0 [\(c + (2 * 1))/] is Nat

proof

then reconsider finerg = [\(c + (2 * 1))/] as Nat ;
[\(c + (2 * 1))/] in INT
by INT_1:def 2;

then consider k being Nat such that

ZZ: ( [\(c + (2 * 1))/] = k or [\(c + (2 * 1))/] = - k ) by INT_1:def 1;

thus [\(c + (2 * 1))/] is Nat by ZZ, WQ; :: thesis: verum

end;then consider k being Nat such that

ZZ: ( [\(c + (2 * 1))/] = k or [\(c + (2 * 1))/] = - k ) by INT_1:def 1;

thus [\(c + (2 * 1))/] is Nat by ZZ, WQ; :: thesis: verum

W0: (c + (2 * 1)) - 1 < finerg by INT_1:def 6;

(c + (2 * 1)) - 1 = c + 1 ;

then W1: c < (c + (2 * 1)) - 1 by XREAL_1:29;

W2: finerg < 0 + (finerg + 1) by XREAL_1:29;

c < finerg by W0, W1, XXREAL_0:2;

then c < 0 + (finerg + 1) by W2, XXREAL_0:2;

then not c in [.(0 + (finerg + 1)),+infty.] by XXREAL_1:1;

then not c in (ext_left_closed_sets 0) . (finerg + 1) by Def4000;

hence contradiction by Y, PROB_1:13; :: thesis: verum

for n being Nat holds c in (ext_left_closed_sets 0) . n

proof

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

s2: (ext_left_closed_sets 0) . n = [.(0 + n),+infty.] by Def4000;

0 + n <= +infty by XXREAL_0:3;

then {+infty} c= [.(0 + n),+infty.] by ZFMISC_1:31, XXREAL_1:1;

hence c in (ext_left_closed_sets 0) . n by A12, s2; :: thesis: verum

end;s2: (ext_left_closed_sets 0) . n = [.(0 + n),+infty.] by Def4000;

0 + n <= +infty by XXREAL_0:3;

then {+infty} c= [.(0 + n),+infty.] by ZFMISC_1:31, XXREAL_1:1;

hence c in (ext_left_closed_sets 0) . n by A12, s2; :: thesis: verum