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

proof

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

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

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

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

end;

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

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

end;

end;

end;

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