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

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