let A be Subset of R^1 ; :: thesis: for a, b being real number st a < b & A = ].-infty ,a.[ \/ ].a,b.[ holds
Cl A = ].-infty ,b.]
let a, b be real number ; :: thesis: ( a < b & A = ].-infty ,a.[ \/ ].a,b.[ implies Cl A = ].-infty ,b.] )
assume that
A1: a < b and
A2: A = ].-infty ,a.[ \/ ].a,b.[ ; :: thesis: Cl A = ].-infty ,b.]
reconsider B = ].-infty ,a.[, C = ].a,b.[ as Subset of R^1 by TOPMETR:24;
A3: Cl C = [.a,b.] by A1, Th36;
Cl A = (Cl B) \/ (Cl C) by A2, PRE_TOPC:50
.= ].-infty ,a.] \/ [.a,b.] by A3, Th77
.= ].-infty ,b.] by A1, Th29 ;
hence Cl A = ].-infty ,b.] ; :: thesis: verum