let A be Subset of R^1; :: thesis: for a, b being Real st a < b & A = ].-infty,a.[ \/ ].a,b.] holds
Cl A = ].-infty,b.]
let a, b be Real; :: 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:17;
A3: Cl C = [.a,b.] by A1, Th35;
Cl A = (Cl B) \/ (Cl C) by A2, PRE_TOPC:20
.= ].-infty,a.] \/ [.a,b.] by A3, Th50
.= ].-infty,b.] by A1, Th11 ;
hence Cl A = ].-infty,b.] ; :: thesis: verum