let k be ExtReal; ExtREAL \ [.-infty,k.] = ].k,+infty.]
for x being object holds
( x in ExtREAL \ [.-infty,k.] iff x in ].k,+infty.] )
proof
let x be
object ;
( x in ExtREAL \ [.-infty,k.] iff x in ].k,+infty.] )
hereby ( x in ].k,+infty.] implies x in ExtREAL \ [.-infty,k.] )
assume A2:
x in ExtREAL \ [.-infty,k.]
;
x in ].k,+infty.]A3:
(
x in [.-infty,+infty.] & not
x in [.-infty,k.] )
by A2, XBOOLE_0:def 5, XXREAL_1:209;
consider y being
Element of
ExtREAL such that A4:
x = y
by A2;
(
y in [.-infty,+infty.] & ( not
-infty <= y or not
y <= k ) )
by A4, A3, XXREAL_1:1;
hence
x in ].k,+infty.]
by XXREAL_1:2, A4, XXREAL_0:3, XXREAL_0:5;
verum
end;
assume A6:
x in ].k,+infty.]
;
x in ExtREAL \ [.-infty,k.]
then
(
k in ExtREAL &
x in ].k,+infty.] &
x in { a where a is Element of ExtREAL : ( k < a & a <= +infty ) } )
by XXREAL_0:def 1, XXREAL_1:def 3;
then consider a being
Element of
ExtREAL such that A7:
(
a = x &
k < a &
a <= +infty )
;
consider y being
Element of
ExtREAL such that A8:
x = y
by A7;
reconsider y =
y as
Element of
ExtREAL ;
y > k
by A6, A8, XXREAL_1:2;
then
(
y in ExtREAL & not
y in [.-infty,k.] )
by XXREAL_1:1;
hence
x in ExtREAL \ [.-infty,k.]
by A8, XBOOLE_0:def 5;
verum
end;
hence
ExtREAL \ [.-infty,k.] = ].k,+infty.]
; verum