let A be Subset of R^1; :: thesis: for a being Real st A = {a} holds
Cl A = {a}
let a be Real; :: 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