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