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

proof

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

hereby :: thesis: verum

let x, y be Point of X; :: thesis: ( x <> y implies Cl {x} <> Cl {y} )
assume A2: x <> y ; :: thesis: Cl {x} <> Cl {y}

now :: thesis: not Cl {x} = Cl {y}

per cases ( ex V being Subset of X st
( V is open & x in V & not y in V ) or ex W being Subset of X st
( W is open & not x in W & y in W ) ) by A1, A2;

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

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: contradiction
hence contradiction by A7, A6, XBOOLE_0:def 7; :: thesis: verum

end;

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

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: contradiction
hence contradiction by A12, A11, XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

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

end;

end;

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

now :: thesis: for x, y being Point of X st x <> y & ( for E being Subset of X st E is closed & x in E holds
y in E ) holds
ex F being Subset of X st
( F is closed & not x in F & y in F )

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

proof

set F = Cl {y};
take Cl {y} ; :: thesis: ( Cl {y} is closed & not x in Cl {y} & y in Cl {y} )
thus Cl {y} is closed ; :: thesis: ( not x in Cl {y} & y in Cl {y} )

now :: thesis: not x in Cl {y}

assume x in Cl {y} ; :: thesis: contradiction
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: verum

end;

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

end;

end;

hence X is T_0 ; :: thesis: verum