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