let p, q be Point of (LinearTopSpaceNorm X); :: according to PRE_TOPC:def 16 :: thesis: ( p = q or ex b₁, b₂ being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ ) )
assume A1: p <> q ; :: thesis: ex b₁, b₂ being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ )
reconsider p1 = p, q1 = q as Point of (TopSpaceNorm X) by Def4;
consider W1, V1 being Subset of (TopSpaceNorm X) such that
A2: ( W1 is open & V1 is open & p1 in W1 & q1 in V1 & W1 misses V1 ) by A1, PRE_TOPC:def 16;
reconsider W = W1, V = V1 as Subset of (LinearTopSpaceNorm X) by Def4;
A3: the topology of (LinearTopSpaceNorm X) = the topology of (TopSpaceNorm X) by Def4;
( W1 in the topology of (TopSpaceNorm X) & V1 in the topology of (TopSpaceNorm X) ) by A2, PRE_TOPC:def 5;
then ( W is open & V is open ) by A3, PRE_TOPC:def 5;
hence ex b₁, b₂ being Element of bool the carrier of (LinearTopSpaceNorm X) st
( b₁ is open & b₂ is open & p in b₁ & q in b₂ & b₁ misses b₂ ) by A2; :: thesis: verum