let k be Real; :: thesis: REAL \ ].-infty,k.[ = [.k,+infty.[

A1: k in REAL by XREAL_0:def 1;

for x being object holds

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

A1: k in REAL by XREAL_0:def 1;

for x being object holds

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

proof

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

then ( k in REAL & x in [.k,+infty.[ & x in { a where a is Element of ExtREAL : ( k <= a & a < +infty ) } ) by XREAL_0:def 1, XXREAL_1:def 2;

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 REAL by A7, A8, A1, XXREAL_0:46;

y >= k by A6, A8, XXREAL_1:236;

then ( y in REAL & not y in ].-infty,k.[ ) by XXREAL_1:233;

hence x in REAL \ ].-infty,k.[ by A8, XBOOLE_0:def 5; :: thesis: verum

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

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

consider y being Element of REAL such that

A4: x = y by A2;

A5: ( y in ].-infty,+infty.[ & not y < k ) by A4, A3, XXREAL_1:233;

thus x in [.k,+infty.[ by A5, A4, XXREAL_1:236; :: thesis: verum

end;A3: ( x in ].-infty,+infty.[ & not x in ].-infty,k.[ ) by A2, XBOOLE_0:def 5, XXREAL_1:224;

consider y being Element of REAL such that

A4: x = y by A2;

A5: ( y in ].-infty,+infty.[ & not y < k ) by A4, A3, XXREAL_1:233;

thus x in [.k,+infty.[ by A5, A4, XXREAL_1:236; :: thesis: verum

then ( k in REAL & x in [.k,+infty.[ & x in { a where a is Element of ExtREAL : ( k <= a & a < +infty ) } ) by XREAL_0:def 1, XXREAL_1:def 2;

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 REAL by A7, A8, A1, XXREAL_0:46;

y >= k by A6, A8, XXREAL_1:236;

then ( y in REAL & not y in ].-infty,k.[ ) by XXREAL_1:233;

hence x in REAL \ ].-infty,k.[ by A8, XBOOLE_0:def 5; :: thesis: verum