thus ( A is T_0 implies for x, y being Point of X st x in A & y in A & x <> y holds
Cl {x} <> Cl {y} ) :: 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:

per cases by A1, A2;

suppose ex V being Subset of X st
( V is open & x in V & not y in V ) ; :: thesis:

then consider V being Subset of X such that
A3: V is open and
A4: x in V and
A5: not y in V ;
y in V ` by A5, SUBSET_1:29;
then {y} c= V ` by ZFMISC_1:31;
then A6: {y} misses V by SUBSET_1:23;
assume A7: Cl {x} = Cl {y} ; :: thesis:
( x in {x} & {x} c= Cl {x} ) by PRE_TOPC:18, TARSKI:def 1;
then Cl {x} meets V by A4, XBOOLE_0:3;
hence contradiction by A3, A6, A7, TSEP_1:36; :: thesis:

end;

suppose ex W being Subset of X st
( W is open & not x in W & y in W ) ; :: thesis:

then consider W being Subset of X such that
A8: W is open and
A9: not x in W and
A10: y in W ;
x in W ` by A9, SUBSET_1:29;
then {x} c= W ` by ZFMISC_1:31;
then A11: {x} misses W by SUBSET_1:23;
assume A12: Cl {x} = Cl {y} ; :: thesis:
( y in {y} & {y} c= Cl {y} ) by PRE_TOPC:18, TARSKI:def 1;
then Cl {y} meets W by A10, XBOOLE_0:3;
hence contradiction by A8, A11, A12, TSEP_1:36; :: thesis:

end;

end;

end;

hence Cl {x} <> Cl {y} ; :: thesis:

end;

end;

assume A13: for x, y being Point of X st x in A & y in A & x <> y holds
Cl {x} <> Cl {y} ; :: thesis:

let x, y be Point of X; :: thesis:
assume A14: ( x in A & y in A & x <> y ) ; :: thesis:
assume A15: for E being Subset of X st E is closed & x in E holds
y in E ; :: thesis:
thus ex F being Subset of X st
( F is closed & not x in F & y in F ) :: thesis:

set F = Cl {y};
take Cl {y} ; :: thesis:
thus Cl {y} is closed ; :: thesis:

assume x in Cl {y} ; :: thesis:
then {x} c= Cl {y} by ZFMISC_1:31;
then A16: Cl {x} c= Cl {y} by TOPS_1:5;
y in Cl {x} by A15, Lm2;
then {y} c= Cl {x} by ZFMISC_1:31;
then Cl {y} c= Cl {x} by TOPS_1:5;
then Cl {x} = Cl {y} by A16, XBOOLE_0:def 10;
hence contradiction by A13, A14; :: thesis:

end;

hence not x in Cl {y} ; :: thesis:
thus y in Cl {y} by Lm2; :: thesis:

end;

end;

hence A is T_0 ; :: thesis: