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

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