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 )

Cl {x} <> Cl {y} ; :: thesis: X is T_0

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 A13:
for x, y being Point of X st x <> y holds
assume A1:
X is T_0
; :: thesis: for x, y being Point of X st x <> y holds

Cl {x} <> Cl {y}

end;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}

end;assume A2: x <> y ; :: thesis: Cl {x} <> Cl {y}

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

hence
Cl {x} <> Cl {y}
; :: thesis: verumper 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;

end;

( 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}

( 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;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

suppose
ex W being Subset of X st

( W is open & not x in W & y in W ) ; :: thesis: not Cl {x} = Cl {y}

( 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;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

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 )

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

end;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} )

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

end;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}

hence
not x in Cl {y}
; :: thesis: y 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;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

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