let k be real number ; :: thesis: REAL \ ].-infty,k.[ = [.k,+infty.[
L: k in REAL by XREAL_0:def 1;
for x being set holds
( x in REAL \ ].-infty,k.[ iff x in [.k,+infty.[ )

proof

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

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

assume AP0: x in REAL \ ].-infty,k.[ ; :: thesis: x in [.k,+infty.[
A0: ( x in ].-infty,+infty.[ & not x in ].-infty,k.[ ) by AP0, XBOOLE_0:def 5, XXREAL_1:224;
consider y being Element of REAL such that
A01: x = y by AP0;
A1: ( y in ].-infty,+infty.[ & not y < k ) by A01, A0, XXREAL_1:233;
thus x in [.k,+infty.[ by A1, A01, XXREAL_1:236; :: thesis: verum

end;

assume B00: 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
B2: ( a = x & k <= a & a < +infty ) ;
consider y being Element of ExtREAL such that
B20: x = y by B2;
reconsider y = y as Element of REAL by B2, B20, L, XXREAL_0:46;
y >= k by B00, B20, XXREAL_1:236;
then ( y in REAL & not y in ].-infty,k.[ ) by XXREAL_1:233;
hence x in REAL \ ].-infty,k.[ by B20, XBOOLE_0:def 5; :: thesis: verum

end;

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