let A be Subset of R^1; :: thesis: for a, b being Real st a <= b & A = ].-infty,a.] \/ {b} holds
A ` = ].a,b.[ \/ ].b,+infty.[
let a, b be Real; :: thesis: ( a <= b & A = ].-infty,a.] \/ {b} implies A ` = ].a,b.[ \/ ].b,+infty.[ )
assume that
A1: a <= b and
A2: A = ].-infty,a.] \/ {b} ; :: thesis: A ` = ].a,b.[ \/ ].b,+infty.[
A ` = (REAL \ ].-infty,a.]) \ {b} by A2, TOPMETR:17, 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