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;
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;
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