let T be non empty TopSpace; :: thesis: ( T is T_1/2 implies T is T_0 )

assume A1: T is T_1/2 ; :: thesis: T is T_0

assume A1: T is T_1/2 ; :: thesis: T is T_0

now :: thesis: for x, y being Point of T st x <> y & x in Cl {y} holds

not y in Cl {x}

hence
T is T_0
by TSP_1:def 6; :: thesis: verumnot y in Cl {x}

let x, y be Point of T; :: thesis: ( x <> y & x in Cl {y} implies not y in Cl {x} )

assume A2: x <> y ; :: thesis: ( x in Cl {y} implies not y in Cl {x} )

assume that

A3: x in Cl {y} and

A4: y in Cl {x} ; :: thesis: contradiction

ex G being Subset of T st

( G is open & y in G & not {x} meets G )

end;assume A2: x <> y ; :: thesis: ( x in Cl {y} implies not y in Cl {x} )

assume that

A3: x in Cl {y} and

A4: y in Cl {x} ; :: thesis: contradiction

ex G being Subset of T st

( G is open & y in G & not {x} meets G )

proof

hence
contradiction
by A4, PRE_TOPC:24; :: thesis: verum
set X = (Der {x}) ` ;

not x in Der {x}

assume A10: for G being Subset of T st G is open & y in G holds

{x} meets G ; :: thesis: contradiction

for U being open Subset of T st y in U holds

ex r being Point of T st

( r in {x} /\ U & y <> r )

then A12: not y in (Der {x}) ` by XBOOLE_0:def 5;

Der {x} is closed by A1;

then {y} meets (Der {x}) ` by A3, A9, PRE_TOPC:24;

hence contradiction by A12, ZFMISC_1:50; :: thesis: verum

end;not x in Der {x}

proof

then A9:
x in (Der {x}) `
by SUBSET_1:29;
set U = the a_neighborhood of x;

consider V being Subset of T such that

A5: V is open and

V c= the a_neighborhood of x and

A6: x in V by CONNSP_2:6;

assume x in Der {x} ; :: thesis: contradiction

then consider z being Point of T such that

A7: z in {x} /\ V and

A8: x <> z by A5, A6, TOPGEN_1:17;

z in {x} by A7, XBOOLE_0:def 4;

hence contradiction by A8, TARSKI:def 1; :: thesis: verum

end;consider V being Subset of T such that

A5: V is open and

V c= the a_neighborhood of x and

A6: x in V by CONNSP_2:6;

assume x in Der {x} ; :: thesis: contradiction

then consider z being Point of T such that

A7: z in {x} /\ V and

A8: x <> z by A5, A6, TOPGEN_1:17;

z in {x} by A7, XBOOLE_0:def 4;

hence contradiction by A8, TARSKI:def 1; :: thesis: verum

assume A10: for G being Subset of T st G is open & y in G holds

{x} meets G ; :: thesis: contradiction

for U being open Subset of T st y in U holds

ex r being Point of T st

( r in {x} /\ U & y <> r )

proof

then
y in Der {x}
by TOPGEN_1:17;
let U be open Subset of T; :: thesis: ( y in U implies ex r being Point of T st

( r in {x} /\ U & y <> r ) )

assume y in U ; :: thesis: ex r being Point of T st

( r in {x} /\ U & y <> r )

then {x} meets U by A10;

then A11: x in U by ZFMISC_1:50;

x in {x} by TARSKI:def 1;

then x in {x} /\ U by A11, XBOOLE_0:def 4;

hence ex r being Point of T st

( r in {x} /\ U & y <> r ) by A2; :: thesis: verum

end;( r in {x} /\ U & y <> r ) )

assume y in U ; :: thesis: ex r being Point of T st

( r in {x} /\ U & y <> r )

then {x} meets U by A10;

then A11: x in U by ZFMISC_1:50;

x in {x} by TARSKI:def 1;

then x in {x} /\ U by A11, XBOOLE_0:def 4;

hence ex r being Point of T st

( r in {x} /\ U & y <> r ) by A2; :: thesis: verum

then A12: not y in (Der {x}) ` by XBOOLE_0:def 5;

Der {x} is closed by A1;

then {y} meets (Der {x}) ` by A3, A9, PRE_TOPC:24;

hence contradiction by A12, ZFMISC_1:50; :: thesis: verum