let a be real number ; :: thesis: Cl ].a,+infty.[ = [.a,+infty.[
reconsider A = ].a,+infty.[ as Subset of R^1 by TOPMETR:17;
Cl A = [.a,+infty.[ by Th49;
hence Cl ].a,+infty.[ = [.a,+infty.[ by JORDAN5A:24; :: thesis: verum