let a be real number ; :: thesis: [.a,+infty .[ = {a} \/ ].a,+infty .[
thus [.a,+infty .[ c= {a} \/ ].a,+infty .[ :: according to XBOOLE_0:def 10 :: thesis: {a} \/ ].a,+infty .[ c= [.a,+infty .[

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [.a,+infty .[ or x in {a} \/ ].a,+infty .[ )
assume A1: x in [.a,+infty .[ ; :: thesis: x in {a} \/ ].a,+infty .[
then reconsider x = x as real number ;
A2: x >= a by A1, XXREAL_1:236;

per cases ( x = a or x > a ) by A2, XXREAL_0:1;

suppose x = a ; :: thesis: x in {a} \/ ].a,+infty .[

then x in {a} by TARSKI:def 1;
hence x in {a} \/ ].a,+infty .[ by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x > a ; :: thesis: x in {a} \/ ].a,+infty .[

then x in ].a,+infty .[ by XXREAL_1:235;
hence x in {a} \/ ].a,+infty .[ by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {a} \/ ].a,+infty .[ or x in [.a,+infty .[ )
assume A3: x in {a} \/ ].a,+infty .[ ; :: thesis: x in [.a,+infty .[
then reconsider x = x as real number ;
( x in {a} or x in ].a,+infty .[ ) by A3, XBOOLE_0:def 3;
then ( x = a or x > a ) by TARSKI:def 1, XXREAL_1:235;
hence x in [.a,+infty .[ by XXREAL_1:236; :: thesis: verum