let X be LinearTopSpace; :: thesis: ( X is T_1 implies X is Hausdorff )
assume A1: X is T_1 ; :: thesis: X is Hausdorff
let p, q be Point of X; :: according to PRE_TOPC:def 10 :: thesis: ( p = q or ex b₁, b₂ being Element of bool the carrier of X st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ ) )
assume A2: p <> q ; :: thesis: ex b₁, b₂ being Element of bool the carrier of X st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ )
{q} is closed by A1, URYSOHN1:19;
then consider V being a_neighborhood of 0. X such that
A3: {p} + V misses {q} + V by A2, Th57, ZFMISC_1:11;
take p + (Int V) ; :: thesis: ex b₁ being Element of bool the carrier of X st
( p + (Int V) is open & b₁ is open & p in p + (Int V) & q in b₁ & p + (Int V) misses b₁ )
take q + (Int V) ; :: thesis: ( p + (Int V) is open & q + (Int V) is open & p in p + (Int V) & q in q + (Int V) & p + (Int V) misses q + (Int V) )
A4: ( {p} + V = p + V & {q} + V = q + V ) by RUSUB_4:33;
thus ( p + (Int V) is open & q + (Int V) is open ) ; :: thesis: ( p in p + (Int V) & q in q + (Int V) & p + (Int V) misses q + (Int V) )
0. X in Int V by CONNSP_2:def 1;
then ( p + (0. X) in p + (Int V) & q + (0. X) in q + (Int V) ) by Lm1;
hence ( p in p + (Int V) & q in q + (Int V) ) ; :: thesis: p + (Int V) misses q + (Int V)
( p + (Int V) c= p + V & q + (Int V) c= q + V ) by Th8, TOPS_1:16;
hence p + (Int V) misses q + (Int V) by A3, A4, XBOOLE_1:64; :: thesis: verum