for c being object holds

( c in Intersection (ext_right_closed_sets 0) iff c in {-infty} )

( c in Intersection (ext_right_closed_sets 0) iff c in {-infty} )

proof

hence
Intersection (ext_right_closed_sets 0) = {-infty}
; :: thesis: verum
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) )

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

end;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 A12:
c in {-infty}
; :: thesis: c in Intersection (ext_right_closed_sets 0)
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;

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 [.-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;then not c in (ext_right_closed_sets 0) . (0 + 0) by Def3000;

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 [.-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;then not c in (ext_right_closed_sets 0) . (0 + 1) by Def3000;

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

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

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

WQ: [\(((- 1) * c) + 1)/] > 0

not c in (ext_right_closed_sets 0) . (finerg + 1)

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

proof end;

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

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

not c in (ext_right_closed_sets 0) . (finerg + 1)

proof

hence
contradiction
by Y, PROB_1:13; :: thesis: verum
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;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

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

proof

hence
c in Intersection (ext_right_closed_sets 0)
by PROB_1:13; :: thesis: verum
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;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