for c being object holds
( c in Intersection (ext_left_closed_sets 0) iff c in {+infty} )

proof

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) )

proof

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;

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

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;

suppose c in REAL ; :: thesis: contradiction

then reconsider c = c as Element of REAL ;

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

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;

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

proof

c + ((1 + 1) - 1) > 0 by S1;
hence [\(c + (2 * 1))/] > 0 by WQ1; :: thesis: verum

end;

[\(c + (2 * 1))/] is Nat

proof

[\(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 reconsider finerg = [\(c + (2 * 1))/] as 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;

end;

end;

end;

end;

assume A12: c in {+infty} ; :: thesis: c in Intersection (ext_left_closed_sets 0)
for n being Nat holds c in (ext_left_closed_sets 0) . n

proof

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;

hence c in Intersection (ext_left_closed_sets 0) by PROB_1:13; :: thesis: verum

end;

hence Intersection (ext_left_closed_sets 0) = {+infty} ; :: thesis: verum