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