let T be non empty sober TopSpace; :: thesis: T is T_0

for p, q being Point of T st Cl {p} = Cl {q} holds

p = q

for p, q being Point of T st Cl {p} = Cl {q} holds

p = q

proof

hence
T is T_0
by Th23; :: thesis: verum
let p, q be Point of T; :: thesis: ( Cl {p} = Cl {q} implies p = q )

assume A1: Cl {p} = Cl {q} ; :: thesis: p = q

Cl {p} is irreducible by Th17;

then consider r being Point of T such that

r is_dense_point_of Cl {p} and

A2: for q being Point of T st q is_dense_point_of Cl {p} holds

r = q by Def5;

p = r by A2, Th18;

hence p = q by A1, A2, Th18; :: thesis: verum

end;assume A1: Cl {p} = Cl {q} ; :: thesis: p = q

Cl {p} is irreducible by Th17;

then consider r being Point of T such that

r is_dense_point_of Cl {p} and

A2: for q being Point of T st q is_dense_point_of Cl {p} holds

r = q by Def5;

p = r by A2, Th18;

hence p = q by A1, A2, Th18; :: thesis: verum