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