thus ( X is T_0 implies for x, y being Point of X holds
( not x <> y or not x in Cl {y} or not y in Cl {x} ) ) :: thesis: ( ( for x, y being Point of X holds
( not x <> y or not x in Cl {y} or not y in Cl {x} ) ) implies X is T_0 )

proof

assume A1: X is T_0 ; :: thesis: for x, y being Point of X holds
( not x <> y or not x in Cl {y} or not y in Cl {x} )

hereby :: thesis: verum

let x, y be Point of X; :: thesis: ( x <> y & x in Cl {y} implies not y in Cl {x} )
assume A2: x <> y ; :: thesis: ( x in Cl {y} implies not y in Cl {x} )
assume ( x in Cl {y} & y in Cl {x} ) ; :: thesis: contradiction
then ( {x} c= Cl {y} & {y} c= Cl {x} ) by ZFMISC_1:37;
then ( Cl {x} c= Cl {y} & Cl {y} c= Cl {x} ) by TOPS_1:31;
then Cl {x} = Cl {y} by XBOOLE_0:def 10;
hence contradiction by A1, A2, Def5; :: thesis: verum

end;

end;

assume A3: for x, y being Point of X holds
( not x <> y or not x in Cl {y} or not y in Cl {x} ) ; :: thesis: X is T_0
for x, y being Point of X st x <> y holds
Cl {x} <> Cl {y}

proof

let x, y be Point of X; :: thesis: ( x <> y implies Cl {x} <> Cl {y} )
assume A4: x <> y ; :: thesis: Cl {x} <> Cl {y}
assume A5: Cl {x} = Cl {y} ; :: thesis: contradiction

now

per cases ( not x in Cl {y} or not y in Cl {x} ) by A3, A4;

suppose not x in Cl {y} ; :: thesis: contradiction

hence contradiction by A5, Lm2; :: thesis: verum

end;

suppose not y in Cl {x} ; :: thesis: contradiction

hence contradiction by A5, Lm2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence X is T_0 by Def5; :: thesis: verum