let X be RealNormSpace; :: thesis: for S being Subset-Family of (TopSpaceNorm X)
for St being Subset-Family of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is Basis of iff S is Basis of )
let S be Subset-Family of (TopSpaceNorm X); :: thesis: for St being Subset-Family of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is Basis of iff S is Basis of )
let St be Subset-Family of (LinearTopSpaceNorm X); :: thesis: for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is Basis of iff S is Basis of )
let x be Point of (TopSpaceNorm X); :: thesis: for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is Basis of iff S is Basis of )
let xt be Point of (LinearTopSpaceNorm X); :: thesis: ( S = St & x = xt implies ( St is Basis of iff S is Basis of ) )
assume that
A1: S = St and
A2: x = xt ; :: thesis: ( St is Basis of iff S is Basis of )
A3: Intersect S = Intersect St by A1, Def4;

hereby :: thesis: ( S is Basis of implies St is Basis of )

assume A4: St is Basis of ; :: thesis: S is Basis of
then St c= the topology of (LinearTopSpaceNorm X) by TOPS_2:64;
then A5: S c= the topology of (TopSpaceNorm X) by A1, Def4;

A6: now :: thesis: for U being Subset of (TopSpaceNorm X) st U is open & x in U holds
ex V being Subset of (TopSpaceNorm X) st
( V in S & V c= U )

let U be Subset of (TopSpaceNorm X); :: thesis: ( U is open & x in U implies ex V being Subset of (TopSpaceNorm X) st
( V in S & V c= U ) )
assume that
A7: U is open and
A8: x in U ; :: thesis: ex V being Subset of (TopSpaceNorm X) st
( V in S & V c= U )
reconsider Ut = U as open Subset of (LinearTopSpaceNorm X) by A7, Def4, Th20;
consider Vt being Subset of (LinearTopSpaceNorm X) such that
A9: ( Vt in St & Vt c= Ut ) by A2, A4, A8, YELLOW_8:def 1;
reconsider V = Vt as Subset of (TopSpaceNorm X) by Def4;
take V = V; :: thesis: ( V in S & V c= U )
thus ( V in S & V c= U ) by A1, A9; :: thesis: verum

end;

x in Intersect S by A2, A3, A4, YELLOW_8:def 1;
hence S is Basis of by A5, A6, TOPS_2:64, YELLOW_8:def 1; :: thesis: verum

end;

assume A10: S is Basis of ; :: thesis: St is Basis of
then S c= the topology of (TopSpaceNorm X) by TOPS_2:64;
then A11: St c= the topology of (LinearTopSpaceNorm X) by A1, Def4;

A12: now :: thesis: for Ut being Subset of (LinearTopSpaceNorm X) st Ut is open & xt in Ut holds
ex Vt being Subset of (LinearTopSpaceNorm X) st
( Vt in St & Vt c= Ut )

let Ut be Subset of (LinearTopSpaceNorm X); :: thesis: ( Ut is open & xt in Ut implies ex Vt being Subset of (LinearTopSpaceNorm X) st
( Vt in St & Vt c= Ut ) )
assume that
A13: Ut is open and
A14: xt in Ut ; :: thesis: ex Vt being Subset of (LinearTopSpaceNorm X) st
( Vt in St & Vt c= Ut )
reconsider U = Ut as open Subset of (TopSpaceNorm X) by A13, Def4, Th20;
consider V being Subset of (TopSpaceNorm X) such that
A15: ( V in S & V c= U ) by A2, A10, A14, YELLOW_8:def 1;
reconsider Vt = V as Subset of (LinearTopSpaceNorm X) by Def4;
take Vt = Vt; :: thesis: ( Vt in St & Vt c= Ut )
thus ( Vt in St & Vt c= Ut ) by A1, A15; :: thesis: verum

end;

xt in Intersect St by A2, A3, A10, YELLOW_8:def 1;
hence St is Basis of by A11, A12, TOPS_2:64, YELLOW_8:def 1; :: thesis: verum