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;
consider G2 being Subset of T such that
A4: ( G2 is open & q in G2 & p in G2 ` ) by A1, A2;
take G1 ; :: thesis: ex V being Subset of T st
( G1 is open & V is open & p in G1 & not q in G1 & q in V & not p in V )

take G2 ; :: thesis: ( G1 is open & G2 is open & p in G1 & not q in G1 & q in G2 & not p in G2 )
thus ( G1 is open & G2 is open & p in G1 & not q in G1 & q in G2 & not p in G2 ) by ; :: 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 9 :: thesis: ( p = q or ex b1 being Element of bool the carrier of T st
( b1 is open & p in b1 & q in b1 ` ) )

assume p <> q ; :: thesis: ex b1 being Element of bool the carrier of T st
( b1 is open & p in b1 & q in b1 ` )

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 W ; :: thesis: ( W is open & p in W & q in W ` )
thus ( W is open & p in W & q in W ` ) by ; :: thesis: verum