let k be Real; 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 ;
( x in REAL \ ].-infty,k.[ iff x in [.k,+infty.[ )
hereby ( x in [.k,+infty.[ implies x in REAL \ ].-infty,k.[ )
assume A2:
x in REAL \ ].-infty,k.[
;
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;
verum
end;
assume A6:
x in [.k,+infty.[
;
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;
verum
end;
hence
REAL \ ].-infty,k.[ = [.k,+infty.[
by TARSKI:2; verum