A1: ].-infty ,1.[ c= ].-infty ,2.]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ].-infty ,1.[ or x in ].-infty ,2.] )
assume A2: x in ].-infty ,1.[ ; :: thesis: x in ].-infty ,2.]
then reconsider x = x as real number ;
x < 1 by A2, XXREAL_1:233;
then x < 2 by XXREAL_0:2;
hence x in ].-infty ,2.] by XXREAL_1:234; :: thesis: verum

end;

[.1,+infty .[ misses ].-infty ,1.[ by XXREAL_1:94;
then A3: ((IRRAT 2,4) \/ {4}) \/ {5} misses ].-infty ,1.[ by Lm9, Lm10, XBOOLE_1:1, XBOOLE_1:63;
].-infty ,1.[ /\ (((].-infty ,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5}) = ].-infty ,1.[ /\ (].-infty ,2.] \/ (((IRRAT 2,4) \/ {4}) \/ {5})) by XBOOLE_1:113
.= ].-infty ,1.[ /\ ].-infty ,2.] by A3, XBOOLE_1:78
.= ].-infty ,1.[ by A1, XBOOLE_1:28 ;
hence ].-infty ,1.[ /\ (((].-infty ,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5}) = ].-infty ,1.[ ; :: thesis: verum