].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 Lm7, 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