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

proof

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

per cases ( x in ].-infty,2.] or x in IRRAT (2,4) ) by A2, XBOOLE_0:def 3;

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

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

end;

suppose x in IRRAT (2,4) ; :: thesis: x in ].-infty,4.]

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

end;

end;

end;

let A be Subset of R^1; :: thesis: ( A = ((RAT (2,4)) \/ ].4,5.[) \/ ].5,+infty.[ implies A ` = ((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5} )
A3: ].4,5.[ \/ ].5,+infty.[ c= ].4,+infty.[

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ].4,5.[ \/ ].5,+infty.[ or x in ].4,+infty.[ )
assume A4: x in ].4,5.[ \/ ].5,+infty.[ ; :: thesis: x in ].4,+infty.[
then reconsider x = x as Real ;

per cases ( x in ].4,5.[ or x in ].5,+infty.[ ) by A4, XBOOLE_0:def 3;

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

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

end;

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

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

end;

end;

end;

assume A = ((RAT (2,4)) \/ ].4,5.[) \/ ].5,+infty.[ ; :: thesis: A ` = ((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}
then A5: A ` = REAL \ ((RAT (2,4)) \/ (].4,5.[ \/ ].5,+infty.[)) by TOPMETR:17, 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 Th57 ;
].-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 Th58
.= ((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5} by XBOOLE_1:4 ;
hence A ` = ((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5} ; :: thesis: verum