let X be RealNormSpace; :: thesis: for S being Subset-Family of ()
for St being Subset-Family of
for x being Point of ()
for xt being Point of st S = St & x = xt holds
( St is Basis of iff S is Basis of )

let S be Subset-Family of (); :: thesis: for St being Subset-Family of
for x being Point of ()
for xt being Point of st S = St & x = xt holds
( St is Basis of iff S is Basis of )

let St be Subset-Family of ; :: thesis: for x being Point of ()
for xt being Point of st S = St & x = xt holds
( St is Basis of iff S is Basis of )

let x be Point of (); :: thesis: for xt being Point of st S = St & x = xt holds
( St is Basis of iff S is Basis of )

let xt be Point of ; :: 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 ;
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 by TOPS_2:64;
then A5: S c= the topology of () by ;
A6: now :: thesis: for U being Subset of () st U is open & x in U holds
ex V being Subset of () st
( V in S & V c= U )
let U be Subset of (); :: thesis: ( U is open & x in U implies ex V being Subset of () st
( V in S & V c= U ) )

assume that
A7: U is open and
A8: x in U ; :: thesis: ex V being Subset of () st
( V in S & V c= U )

reconsider Ut = U as open Subset of by ;
consider Vt being Subset of such that
A9: ( Vt in St & Vt c= Ut ) by ;
reconsider V = Vt as Subset of () 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 ;
hence S is Basis of by ; :: thesis: verum
end;
assume A10: S is Basis of ; :: thesis: St is Basis of
then S c= the topology of () by TOPS_2:64;
then A11: St c= the topology of by ;
A12: now :: thesis: for Ut being Subset of st Ut is open & xt in Ut holds
ex Vt being Subset of st
( Vt in St & Vt c= Ut )
let Ut be Subset of ; :: thesis: ( Ut is open & xt in Ut implies ex Vt being Subset of st
( Vt in St & Vt c= Ut ) )

assume that
A13: Ut is open and
A14: xt in Ut ; :: thesis: ex Vt being Subset of st
( Vt in St & Vt c= Ut )

reconsider U = Ut as open Subset of () by ;
consider V being Subset of () such that
A15: ( V in S & V c= U ) by ;
reconsider Vt = V as Subset of by Def4;
take Vt = Vt; :: thesis: ( Vt in St & Vt c= Ut )
thus ( Vt in St & Vt c= Ut ) by ; :: thesis: verum
end;
xt in Intersect St by ;
hence St is Basis of by ; :: thesis: verum