let A be Subset of R^1 ; :: thesis: for a being real number st A = {a} holds
Cl A = {a}
let a be real number ; :: thesis: ( A = {a} implies Cl A = {a} )
assume A1: A = {a} ; :: thesis: Cl A = {a}
a is Point of R^1 by TOPMETR:24, XREAL_0:def 1;
hence Cl A = {a} by A1, YELLOW_8:35; :: thesis: verum