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₂ ) )
A1: the topology of (LinearTopSpaceNorm X) = the topology of (TopSpaceNorm X) by Def4;
reconsider p1 = p, q1 = q as Point of (TopSpaceNorm X) by Def4;
assume 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₂ )
then consider W1, V1 being Subset of (TopSpaceNorm X) such that
A2: W1 is open and
A3: V1 is open and
A4: ( p1 in W1 & q1 in V1 & W1 misses V1 ) by PRE_TOPC:def 16;
reconsider W = W1, V = V1 as Subset of (LinearTopSpaceNorm X) by Def4;
V1 in the topology of (TopSpaceNorm X) by A3, PRE_TOPC:def 5;
then A5: V is open by A1, PRE_TOPC:def 5;
W1 in the topology of (TopSpaceNorm X) by A2, PRE_TOPC:def 5;
then W is open by A1, 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 A4, A5; :: thesis: verum