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 in REAL ; :: thesis: contradiction
then reconsider c = c as Element of REAL ;
per cases ( c >= 0 or c < 0 ) ;
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