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 xt iff S is Basis of x )
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 xt iff S is Basis of x )
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 xt iff S is Basis of x )
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 xt iff S is Basis of x )
let xt be Point of (LinearTopSpaceNorm X); :: thesis: ( S = St & x = xt implies ( St is Basis of xt iff S is Basis of x ) )
assume A1: ( S = St & x = xt ) ; :: thesis: ( St is Basis of xt iff S is Basis of x )
then A2: Intersect S = Intersect St by Def4;

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

assume A3: St is Basis of xt ; :: thesis: S is Basis of x
then St c= the topology of (LinearTopSpaceNorm X) by YELLOW_8:def 2;
then A4: S c= the topology of (TopSpaceNorm X) by A1, Def4;
A5: x in Intersect S by A1, A2, A3, YELLOW_8:def 2;

now

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 A6: ( U is open & 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 A6, Def4, Th20;
consider Vt being Subset of (LinearTopSpaceNorm X) such that
A7: ( Vt in St & Vt c= Ut ) by A1, A3, A6, YELLOW_8:def 2;
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, A7; :: thesis: verum

end;

hence S is Basis of x by A4, A5, YELLOW_8:def 2; :: thesis: verum

end;

assume A8: S is Basis of x ; :: thesis: St is Basis of xt
then S c= the topology of (TopSpaceNorm X) by YELLOW_8:def 2;
then A9: St c= the topology of (LinearTopSpaceNorm X) by A1, Def4;
A10: xt in Intersect St by A1, A2, A8, YELLOW_8:def 2;

now

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 A11: ( Ut is open & 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 A11, Def4, Th20;
consider V being Subset of (TopSpaceNorm X) such that
A12: ( V in S & V c= U ) by A1, A8, A11, YELLOW_8:def 2;
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, A12; :: thesis: verum

end;

hence St is Basis of xt by A9, A10, YELLOW_8:def 2; :: thesis: verum