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 Th26;
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 Def6;
p = r by A2, Th27;
hence p = q by A1, A2, Th27; :: thesis: verum

end;

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