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