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} )
assume A = ((RAT 2,4) \/ ].4,5.[) \/ ].5,+infty .[ ; :: thesis: A ` = ((].-infty ,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5}
then A1: 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 ;
A2: ].-infty ,4.] misses ].4,+infty .[ by XXREAL_1:91;
A3: ].-infty ,2.] \/ (IRRAT 2,4) c= ].-infty ,4.]

proof

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

per cases ( x in ].-infty ,2.] or x in IRRAT 2,4 ) by A4, 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 Th53;
hence x in ].-infty ,4.] by XXREAL_1:234; :: thesis: verum

end;

end;

end;

].4,5.[ \/ ].5,+infty .[ c= ].4,+infty .[

proof

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

per cases ( x in ].4,5.[ or x in ].5,+infty .[ ) by A5, 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;

then A ` = ([.4,+infty .[ \ (].4,5.[ \/ ].5,+infty .[)) \/ (].-infty ,2.] \/ (IRRAT 2,4)) by A1, A2, 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: verum