(].-infty ,1.[ \/ ].1,+infty .[) /\ (((].-infty ,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5}) = ].-infty ,1.[ \/ (].1,+infty .[ /\ (((].-infty ,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5})) by Lm11, XBOOLE_1:23
.= ].-infty ,1.[ \/ ((].1,2.] \/ (IRRAT 2,4)) \/ ({4} \/ {5})) by Lm12, 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