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

proof

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;

hence T is T_0 by Th23; :: thesis: verum