(].-infty,1.[ \/ ].1,+infty.[) /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = ].-infty,1.[ \/ (].1,+infty.[ /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5})) by Lm9, XBOOLE_1:23
.= ].-infty,1.[ \/ ((].1,2.] \/ (IRRAT (2,4))) \/ ({4} \/ {5})) by Lm10, XBOOLE_1:4
.= ((].-infty,1.[ \/ ].1,2.]) \/ (IRRAT (2,4))) \/ ({4} \/ {5}) by XBOOLE_1:113 ;
hence (].-infty,1.[ \/ ].1,+infty.[) /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = (((].-infty,1.[ \/ ].1,2.]) \/ (IRRAT (2,4))) \/ {4}) \/ {5} by XBOOLE_1:4; :: thesis: verum