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

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