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

proof

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

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

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

hence REAL \ [.k,+infty.[ = ].-infty,k.[ by TARSKI:2; :: thesis: verum