let p, q be Point of (LinearTopSpaceNorm X); :: according to PRE_TOPC:def 10 :: thesis: ( p = q or ex b_{1}, b_{2} being Element of bool the carrier of (LinearTopSpaceNorm X) st

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

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_{1}, b_{2} being Element of bool the carrier of (LinearTopSpaceNorm X) st

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

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 10;

reconsider W = W1, V = V1 as Subset of (LinearTopSpaceNorm X) by Def4;

V1 in the topology of (TopSpaceNorm X) by A3;

then A5: V is open by A1;

W1 in the topology of (TopSpaceNorm X) by A2;

then W is open by A1;

hence ex b_{1}, b_{2} being Element of bool the carrier of (LinearTopSpaceNorm X) st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} )
by A4, A5; :: thesis: verum

( 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

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 10;

reconsider W = W1, V = V1 as Subset of (LinearTopSpaceNorm X) by Def4;

V1 in the topology of (TopSpaceNorm X) by A3;

then A5: V is open by A1;

W1 in the topology of (TopSpaceNorm X) by A2;

then W is open by A1;

hence ex b

( b