let A be Subset of R^1; for a, b being Real st a <= b & A = {a} \/ [.b,+infty.[ holds
A ` = ].-infty,a.[ \/ ].a,b.[
let a, b be Real; ( a <= b & A = {a} \/ [.b,+infty.[ implies A ` = ].-infty,a.[ \/ ].a,b.[ )
assume that
A1:
a <= b
and
A2:
A = {a} \/ [.b,+infty.[
; A ` = ].-infty,a.[ \/ ].a,b.[
A ` =
(REAL \ [.b,+infty.[) \ {a}
by A2, TOPMETR:17, XBOOLE_1:41
.=
].-infty,b.[ \ {a}
by XXREAL_1:224, XXREAL_1:294
;
hence
A ` = ].-infty,a.[ \/ ].a,b.[
by A1, XXREAL_1:349; verum