let T be non empty TopSpace; :: thesis: ( T is T_0 iff for p, q being Point of T st Cl {p} = Cl {q} holds
p = q )
thus ( T is T_0 implies for p, q being Point of T st Cl {p} = Cl {q} holds
p = q ) by TSP_1:def 5; :: thesis: ( ( for p, q being Point of T st Cl {p} = Cl {q} holds
p = q ) implies T is T_0 )
assume for p, q being Point of T st Cl {p} = Cl {q} holds
p = q ; :: thesis: T is T_0
then for p, q being Point of T st p <> q holds
Cl {p} <> Cl {q} ;
hence T is T_0 by TSP_1:def 5; :: thesis: verum