thus ( X is T_0 implies for x, y being Point of X st x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x} ) :: thesis: ( ( for x, y being Point of X st x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x} ) implies X is T_0 )
proof
assume A1: X is T_0 ; :: thesis: for x, y being Point of X st x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x}

hereby :: thesis: verum
let x, y be Point of X; :: thesis: ( x <> y & x in Cl {y} implies not Cl {y} c= Cl {x} )
assume A2: x <> y ; :: thesis: ( x in Cl {y} implies not Cl {y} c= Cl {x} )
assume x in Cl {y} ; :: thesis: not Cl {y} c= Cl {x}
then {x} c= Cl {y} by ZFMISC_1:31;
then A3: Cl {x} c= Cl {y} by TOPS_1:5;
assume Cl {y} c= Cl {x} ; :: thesis: contradiction
then Cl {x} = Cl {y} by ;
hence contradiction by A1, A2; :: thesis: verum
end;
end;
assume A4: for x, y being Point of X st x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x} ; :: thesis: X is T_0
for x, y being Point of X holds
( not x <> y or not x in Cl {y} or not y in Cl {x} )
proof
let x, y be Point of X; :: thesis: ( not x <> y or not x in Cl {y} or not y in Cl {x} )
assume A5: x <> y ; :: thesis: ( not x in Cl {y} or not y in Cl {x} )
assume A6: x in Cl {y} ; :: thesis: not y in Cl {x}
assume y in Cl {x} ; :: thesis: contradiction
then {y} c= Cl {x} by ZFMISC_1:31;
hence contradiction by A4, A5, A6, TOPS_1:5; :: thesis: verum
end;
hence X is T_0 ; :: thesis: verum