thus ( X is T_0 implies for x, y being Point of X st x <> y holds
Cl {x} <> Cl {y} ) :: thesis:

proof

assume A1: X is T_0 ; :: thesis:

hereby :: thesis:

let x, y be Point of X; :: thesis:
assume A2: x <> y ; :: thesis:

now :: 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 ;
( x in {x} & {x} c= Cl {x} ) by PRE_TOPC:18, TARSKI:def 1;
then A6: (Cl {x}) /\ V <> {} by A4, XBOOLE_0:def 4;
y in V ` by A5, SUBSET_1:29;
then {y} c= V ` by ZFMISC_1:31;
then {y} misses V by SUBSET_1:23;
then A7: Cl {y} misses V by A3, TSEP_1:36;
assume Cl {x} = Cl {y} ; :: thesis:
hence contradiction by A7, A6, XBOOLE_0:def 7; :: 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 ;
( y in {y} & {y} c= Cl {y} ) by PRE_TOPC:18, TARSKI:def 1;
then A11: (Cl {y}) /\ W <> {} by A10, XBOOLE_0:def 4;
x in W ` by A9, SUBSET_1:29;
then {x} c= W ` by ZFMISC_1:31;
then {x} misses W by SUBSET_1:23;
then A12: Cl {x} misses W by A8, TSEP_1:36;
assume Cl {x} = Cl {y} ; :: thesis:
hence contradiction by A12, A11, XBOOLE_0:def 7; :: thesis:

end;

end;

end;

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

end;

end;

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

now :: thesis:

let x, y be Point of X; :: thesis:
assume A14: 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:

proof

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

now :: 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 X is T_0 ; :: thesis: