for c being object holds
( c in Intersection (ext_right_closed_sets 0) iff c in {-infty} )

proof

let c be object ; :: thesis: ( c in Intersection (ext_right_closed_sets 0) iff c in {-infty} )
thus ( c in Intersection (ext_right_closed_sets 0) implies c in {-infty} ) :: thesis: ( c in {-infty} implies c in Intersection (ext_right_closed_sets 0) )

proof

assume Y: c in Intersection (ext_right_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 [.-infty,(0 - 0).] by XXREAL_1:1;
then not c in (ext_right_closed_sets 0) . (0 + 0) by Def3000;
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 [.-infty,(0 - (0 + 1)).] by XXREAL_1:1;
then not c in (ext_right_closed_sets 0) . (0 + 1) by Def3000;
hence contradiction by Y, PROB_1:13; :: thesis: verum

end;

suppose S1: c < 0 ; :: thesis: contradiction

set finerg = [\(((- 1) * c) + 1)/];
WQ: [\(((- 1) * c) + 1)/] > 0

proof

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

end;

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

proof

[\(((- 1) * c) + 1)/] in INT by INT_1:def 2;
then consider k being Nat such that
ZZ: ( [\(((- 1) * c) + 1)/] = k or [\(((- 1) * c) + 1)/] = - k ) by INT_1:def 1;
thus [\(((- 1) * c) + 1)/] is Nat by ZZ, WQ; :: thesis: verum

end;

then reconsider finerg = [\(((- 1) * c) + 1)/] as Nat ;
not c in (ext_right_closed_sets 0) . (finerg + 1)

proof

z0: (((- 1) * c) + 1) - 1 < finerg by INT_1:def 6;
finerg < finerg + 1 by XREAL_1:29;
then ((- 1) * c) + 0 < finerg + 1 by z0, XXREAL_0:2;
then - (((- 1) * c) + 0) > - (finerg + 1) by XREAL_1:24;
then not c in [.-infty,(0 - (finerg + 1)).] by XXREAL_1:1;
hence not c in (ext_right_closed_sets 0) . (finerg + 1) by Def3000; :: thesis: verum

end;

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

end;

end;

end;

end;

end;

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

proof

let n be Nat; :: thesis: c in (ext_right_closed_sets 0) . n
s2: (ext_right_closed_sets 0) . n = [.-infty,(0 - n).] by Def3000;
[.-infty,(0 - n).] = {-infty} \/ ].-infty,(0 - n).] by XXREAL_1:421;
then {-infty} c= [.-infty,(0 - n).] by XBOOLE_1:7;
hence c in (ext_right_closed_sets 0) . n by A12, s2; :: thesis: verum

end;

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

end;

hence Intersection (ext_right_closed_sets 0) = {-infty} ; :: thesis: verum