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: ( ( 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} ) implies A is T_0 )

not Cl {y} c= Cl {x} ; :: thesis: A is T_0

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}

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 Cl {y} c= Cl {x} ) implies A is T_0 )

proof

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

end;not Cl {y} c= 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 Cl {y} c= Cl {x} )

assume A2: ( x in A & y in A & 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 A3, XBOOLE_0:def 10;

hence contradiction by A1, A2; :: thesis: verum

end;assume A2: ( x in A & y in A & 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 A3, XBOOLE_0:def 10;

hence contradiction by A1, A2; :: thesis: verum

not Cl {y} c= Cl {x} ; :: thesis: A is T_0

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}

proof

hence
A is T_0
; :: 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 A5: ( x in A & y in A & 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;assume A5: ( x in A & y in A & 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