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