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:
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 ;
then A6: (Cl {x}) /\ V <> {} by ;
y in V ` by ;
then {y} c= V ` by ZFMISC_1:31;
then {y} misses V by SUBSET_1:23;
then A7: Cl {y} misses V by ;
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 ;
then A11: (Cl {y}) /\ W <> {} by ;
x in W ` by ;
then {x} c= W ` by ZFMISC_1:31;
then {x} misses W by SUBSET_1:23;
then A12: Cl {x} misses W by ;
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} )
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