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