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

A1: k in REAL by XREAL_0:def 1;

for x being object holds

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

A1: k in REAL by XREAL_0:def 1;

for x being object holds

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

proof

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

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

then consider a being Element of ExtREAL such that

A6: ( a = x & -infty < a & a < k ) ;

consider y being Element of ExtREAL such that

A7: x = y by A6;

reconsider y = y as Element of REAL by A1, A6, A7, XXREAL_0:47;

y < k by A5, A7, XXREAL_1:233;

then ( y in REAL & not y in [.k,+infty.[ ) by XXREAL_1:236;

hence x in REAL \ [.k,+infty.[ by A7, XBOOLE_0:def 5; :: thesis: verum

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

assume A5:
x in ].-infty,k.[
; :: thesis: x in REAL \ [.k,+infty.[assume A2:
x in REAL \ [.k,+infty.[
; :: thesis: x in ].-infty,k.[

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

consider y being Element of REAL such that

A4: x = y by A2;

( y in ].-infty,+infty.[ & not y >= k ) by A4, A3, XXREAL_1:236;

hence x in ].-infty,k.[ by A4, XXREAL_1:233; :: thesis: verum

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

consider y being Element of REAL such that

A4: x = y by A2;

( y in ].-infty,+infty.[ & not y >= k ) by A4, A3, XXREAL_1:236;

hence x in ].-infty,k.[ by A4, XXREAL_1:233; :: thesis: verum

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

then consider a being Element of ExtREAL such that

A6: ( a = x & -infty < a & a < k ) ;

consider y being Element of ExtREAL such that

A7: x = y by A6;

reconsider y = y as Element of REAL by A1, A6, A7, XXREAL_0:47;

y < k by A5, A7, XXREAL_1:233;

then ( y in REAL & not y in [.k,+infty.[ ) by XXREAL_1:236;

hence x in REAL \ [.k,+infty.[ by A7, XBOOLE_0:def 5; :: thesis: verum