let T be non empty TopSpace; :: thesis: for S being Subset of T st S is closed holds
for p being Point of T st p is_dense_point_of S holds
S = Cl {p}
let S be Subset of T; :: thesis: ( S is closed implies for p being Point of T st p is_dense_point_of S holds
S = Cl {p} )
assume A1: S is closed ; :: thesis: for p being Point of T st p is_dense_point_of S holds
S = Cl {p}
let p be Point of T; :: thesis: ( p is_dense_point_of S implies S = Cl {p} )
assume that
A2: p in S and
A3: S c= Cl {p} ; :: according to YELLOW_8:def 5 :: thesis: S = Cl {p}
{p} c= S by A2, ZFMISC_1:37;
then Cl {p} c= S by A1, TOPS_1:31;
hence S = Cl {p} by A3, XBOOLE_0:def 10; :: thesis: verum