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 Cl {y} c= Cl {x} ) :: thesis:

assume A1: A is T_0 ; :: thesis:

hereby :: thesis:

let x, y be Point of X; :: thesis:
assume A2: ( x in A & y in A & x <> y ) ; :: thesis:
assume x in Cl {y} ; :: thesis:
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:
then Cl {x} = Cl {y} by A3, XBOOLE_0:def 10;
hence contradiction by A1, A2; :: thesis:

end;

end;

assume A4: for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds
not Cl {y} c= 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}

let x, y be Point of X; :: thesis:
assume A5: ( x in A & y in A & x <> y ) ; :: thesis:
assume A6: x in Cl {y} ; :: thesis:
assume y in Cl {x} ; :: thesis:
then {y} c= Cl {x} by ZFMISC_1:31;
hence contradiction by A4, A5, A6, TOPS_1:5; :: thesis:

end;

hence A is T_0 ; :: thesis: