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.] )

for x being object holds

( x in ExtREAL \ [.-infty,k.] iff x in ].k,+infty.] )

proof

hence
ExtREAL \ [.-infty,k.] = ].k,+infty.]
; :: thesis: verum
let x be object ; :: thesis: ( x in ExtREAL \ [.-infty,k.] iff x in ].k,+infty.] )

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

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

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