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;

then S c= the topology of (TopSpaceNorm X) by TOPS_2:64;

then A11: St c= the topology of (LinearTopSpaceNorm X) by A1, Def4;

hence St is Basis of by A11, A12, TOPS_2:64, YELLOW_8:def 1; :: thesis: verum

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 A10:
S is Basis of
; :: thesis: 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;

hence S is Basis of by A5, A6, TOPS_2:64, YELLOW_8:def 1; :: thesis: verum

end;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 )

x in Intersect S
by A2, A3, A4, YELLOW_8:def 1;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;( 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

hence S is Basis of by A5, A6, TOPS_2:64, YELLOW_8:def 1; :: thesis: verum

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 )

xt in Intersect St
by A2, A3, A10, YELLOW_8:def 1;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;( 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

hence St is Basis of by A11, A12, TOPS_2:64, YELLOW_8:def 1; :: thesis: verum