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

proof

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

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

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

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