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 )

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_{1} being Element of bool the carrier of T st

( b_{1} is open & p in b_{1} & q in b_{1} ` ) )

assume p <> q ; :: thesis: ex b_{1} being Element of bool the carrier of T st

( b_{1} is open & p in b_{1} & q in b_{1} ` )

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

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 A5:
for p, q being Point of T st not p = q holds
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 A3, A4, XBOOLE_0:def 5; :: thesis: verum

end;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 A3, A4, XBOOLE_0:def 5; :: thesis: verum

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

( b

assume p <> q ; :: thesis: ex b

( b

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