thus ( T is T_1 implies for p, q being Point of T st not p = q holds
ex W, V being Subset of T st
( W is open & V is open & p in W & not q in W & q in V & not p in V ) ) :: thesis: ( ( for p, q being Point of T st not p = q holds
ex W, V being Subset of T st
( W is open & V is open & p in W & not q in W & q in V & not p in V ) ) implies T is T_1 )

proof

assume A1: T is T_1 ; :: thesis: for p, q being Point of T st not p = q holds
ex W, V being Subset of T st
( W is open & V is open & p in W & not q in W & q in V & not p in V )
let p, q be Point of T; :: thesis: ( not p = q implies ex W, V being Subset of T st
( W is open & V is open & p in W & not q in W & q in V & not p in V ) )
assume A2: not p = q ; :: thesis: ex W, V being Subset of T st
( W is open & V is open & p in W & not q in W & q in V & not p in V )
consider G1 being Subset of T such that
A3: ( G1 is open & p in G1 & q in G1 ` ) by A1, A2, PRE_TOPC:def 15;
consider G2 being Subset of T such that
A4: ( G2 is open & q in G2 & p in G2 ` ) by A1, A2, PRE_TOPC:def 15;
take W = G1; :: thesis: ex V being Subset of T st
( W is open & V is open & p in W & not q in W & q in V & not p in V )
take V = G2; :: thesis: ( W is open & V is open & p in W & not q in W & q in V & not p in V )
thus ( W is open & V is open & p in W & not q in W & q in V & not p in V ) by A3, A4, XBOOLE_0:def 5; :: thesis: verum

end;

assume A5: for p, q being Point of T st not p = q holds
ex W, V being Subset of T st
( W is open & V is open & p in W & not q in W & q in V & not p in V ) ; :: thesis: T is T_1
let p, q be Point of T; :: according to PRE_TOPC:def 15 :: thesis: ( p = q or ex b₁ being Element of bool the carrier of T st
( b₁ is open & p in b₁ & q in b₁ ` ) )
assume p <> q ; :: thesis: ex b<sub>1</sub> being Element of bool the carrier of T st
( b<sub>1</sub> is open & p in b<sub>1</sub> & q in b<sub>1</sub> ` )
then consider W, V being Subset of T such that
A6: W is open and
V is open and
A7: ( p in W & not q in W ) and
q in V and
not p in V by A5;
take G = W; :: thesis: ( G is open & p in G & q in G ` )
thus ( G is open & p in G & q in G ` ) by A6, A7, XBOOLE_0:def 5; :: thesis: verum