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 Th75;
hence Cl ].a,+infty.[ = [.a,+infty.[ by TOPREAL6:71; :: thesis: verum