let A be Subset of R^1 ; :: thesis: for a, b being real number st a <= b & A = ].-infty ,a.] \/ {b} holds
A ` = ].a,b.[ \/ ].b,+infty .[
let a, b be real number ; :: thesis: ( a <= b & A = ].-infty ,a.] \/ {b} implies A ` = ].a,b.[ \/ ].b,+infty .[ )
assume A1: ( a <= b & A = ].-infty ,a.] \/ {b} ) ; :: thesis: A ` = ].a,b.[ \/ ].b,+infty .[
then A ` = (REAL \ ].-infty ,a.]) \ {b} by TOPMETR:24, XBOOLE_1:41
.= ].a,+infty .[ \ {b} by XXREAL_1:224, XXREAL_1:288
.= ].a,b.[ \/ ].b,+infty .[ by A1, XXREAL_1:365 ;
hence A ` = ].a,b.[ \/ ].b,+infty .[ ; :: thesis: verum