let T be non empty TopSpace; :: thesis: for p being Point of T holds p is_dense_point_of Cl {p}
let p be Point of T; :: thesis: p is_dense_point_of Cl {p}
( {p} c= Cl {p} & p in {p} ) by PRE_TOPC:18, TARSKI:def 1;
hence p in Cl {p} ; :: according to YELLOW_8:def 4 :: thesis: Cl {p} c= Cl {p}
thus Cl {p} c= Cl {p} ; :: thesis: verum