let A be Subset of R^1; :: thesis: for a, b being Real st a < b & A = [.a,b.[ \/ ].b,+infty.[ holds
Cl A = [.a,+infty.[
let a, b be Real; :: thesis: ( a < b & A = [.a,b.[ \/ ].b,+infty.[ implies Cl A = [.a,+infty.[ )
assume that
A1: a < b and
A2: A = [.a,b.[ \/ ].b,+infty.[ ; :: thesis: Cl A = [.a,+infty.[
reconsider B = [.a,b.[, C = ].b,+infty.[ as Subset of R^1 by TOPMETR:17;
A3: Cl A = (Cl B) \/ (Cl C) by A2, PRE_TOPC:20;
A4: Cl C = [.b,+infty.[ by Th48;
Cl B = [.a,b.] by A1, Th34;
hence Cl A = [.a,+infty.[ by A1, A4, A3, Th10; :: thesis: verum