let X be LinearTopSpace; :: thesis: ( X is T_1 implies X is T_2 )
assume A1: X is T_1 ; :: thesis: X is T_2
let p, q be Point of X; :: according to PRE_TOPC:def 16 :: 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 Z: 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:27;
then consider V being a_neighborhood of 0. X such that
A4: {p} + V misses {q} + V by Z, Th58, ZFMISC_1:17;
A5: ( {p} + V = p + V & {q} + V = q + V ) by RUSUB_4:36;
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) )
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) ) by RLVECT_1:10; :: thesis: p + (Int V) misses q + (Int V)
( p + (Int V) c= p + V & q + (Int V) c= q + V ) by Th8, TOPS_1:44;
hence p + (Int V) misses q + (Int V) by A4, A5, XBOOLE_1:64; :: thesis: verum