let k be ExtReal; :: thesis: 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 ; :: thesis: ( x in ExtREAL \ [.-infty,k.] iff x in ].k,+infty.] )

hereby :: thesis: ( x in ].k,+infty.] implies x in ExtREAL \ [.-infty,k.] )

assume A2: x in ExtREAL \ [.-infty,k.] ; :: thesis: 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; :: thesis: verum

end;

assume A6: x in ].k,+infty.] ; :: thesis: 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; :: thesis: verum

end;

hence ExtREAL \ [.-infty,k.] = ].k,+infty.] ; :: thesis: verum