A1: ].-infty ,2.] \/ (IRRAT 2,4) c= ].-infty ,4.]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A2: x in ].-infty ,2.] \/ (IRRAT 2,4) ; :: thesis:
then reconsider x = x as real number ;

per cases by A2, XBOOLE_0:def 3;

suppose x in ].-infty ,2.] ; :: thesis:

then x <= 2 by XXREAL_1:234;
then x <= 4 by XXREAL_0:2;
hence x in ].-infty ,4.] by XXREAL_1:234; :: thesis:

end;

suppose x in IRRAT 2,4 ; :: thesis:

then x < 4 by Th53;
hence x in ].-infty ,4.] by XXREAL_1:234; :: thesis:

end;

end;

end;

let A be Subset of R^1 ; :: thesis:
A3: ].4,5.[ \/ ].5,+infty .[ c= ].4,+infty .[

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A4: x in ].4,5.[ \/ ].5,+infty .[ ; :: thesis:
then reconsider x = x as real number ;

per cases by A4, XBOOLE_0:def 3;

suppose x in ].4,5.[ ; :: thesis:

then x > 4 by XXREAL_1:4;
hence x in ].4,+infty .[ by XXREAL_1:235; :: thesis:

end;

suppose x in ].5,+infty .[ ; :: thesis:

then x > 5 by XXREAL_1:235;
then x > 4 by XXREAL_0:2;
hence x in ].4,+infty .[ by XXREAL_1:235; :: thesis:

end;

end;

end;

assume A = ((RAT 2,4) \/ ].4,5.[) \/ ].5,+infty .[ ; :: thesis:
then A5: A ` = REAL \ ((RAT 2,4) \/ (].4,5.[ \/ ].5,+infty .[)) by TOPMETR:24, XBOOLE_1:4
.= (REAL \ (RAT 2,4)) \ (].4,5.[ \/ ].5,+infty .[) by XBOOLE_1:41
.= ((].-infty ,2.] \/ (IRRAT 2,4)) \/ [.4,+infty .[) \ (].4,5.[ \/ ].5,+infty .[) by Th85 ;
].-infty ,4.] misses ].4,+infty .[ by XXREAL_1:91;
then A ` = ([.4,+infty .[ \ (].4,5.[ \/ ].5,+infty .[)) \/ (].-infty ,2.] \/ (IRRAT 2,4)) by A5, A1, A3, XBOOLE_1:64, XBOOLE_1:87
.= (].-infty ,2.] \/ (IRRAT 2,4)) \/ ({4} \/ {5}) by Th88
.= ((].-infty ,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5} by XBOOLE_1:4 ;
hence A ` = ((].-infty ,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5} ; :: thesis: