let A be Subset of R^1 ; :: thesis: for a, b being real number st a <= b & A = {a} \/ [.b,+infty .[ holds
A ` = ].-infty ,a.[ \/ ].a,b.[
let a, b be real number ; :: 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:24, 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