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} )
A1: a is Point of R^1 by TOPMETR:17, XREAL_0:def 1;
assume A = {a} ; :: thesis: Cl A = {a}
hence Cl A = {a} by A1, YELLOW_8:26; :: thesis: verum