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
now :: thesis: for x, y being Point of T st x <> y & x in Cl {y} holds
not 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 )
proof
set X = (Der {x}) ` ;
not x in Der {x}
proof
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;
then A9: x in (Der {x}) ` by SUBSET_1:29;
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
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;
then y in Der {x} by TOPGEN_1:17;
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;
hence contradiction by A4, PRE_TOPC:24; :: thesis: verum
end;
hence T is T_0 by TSP_1:def 6; :: thesis: verum