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