A1: ].-infty,1.[ c= ].-infty,2.]
proof
let x be object ; :: 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 ;
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 Lm7, Lm8, 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