let X be RealNormSpace; :: thesis: for U being Subset of (TopSpaceNorm X)
for Ut being Subset of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st U = Ut & x = xt holds
( U is a_neighborhood of x iff Ut is a_neighborhood of xt )
let U be Subset of (TopSpaceNorm X); :: thesis: for Ut being Subset of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st U = Ut & x = xt holds
( U is a_neighborhood of x iff Ut is a_neighborhood of xt )
let Ut be Subset of (LinearTopSpaceNorm X); :: thesis: for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st U = Ut & x = xt holds
( U is a_neighborhood of x iff Ut is a_neighborhood of xt )
let x be Point of (TopSpaceNorm X); :: thesis: for xt being Point of (LinearTopSpaceNorm X) st U = Ut & x = xt holds
( U is a_neighborhood of x iff Ut is a_neighborhood of xt )
let xt be Point of (LinearTopSpaceNorm X); :: thesis: ( U = Ut & x = xt implies ( U is a_neighborhood of x iff Ut is a_neighborhood of xt ) )
assume A1: ( U = Ut & x = xt ) ; :: thesis: ( U is a_neighborhood of x iff Ut is a_neighborhood of xt )

hereby :: thesis: ( Ut is a_neighborhood of xt implies U is a_neighborhood of x )

assume U is a_neighborhood of x ; :: thesis: Ut is a_neighborhood of xt
then consider V being Subset of (TopSpaceNorm X) such that
A2: ( V is open & V c= U & x in V ) by CONNSP_2:8;
reconsider Vt = V as open Subset of (LinearTopSpaceNorm X) by A2, Def4, Th20;
( Vt is open & Vt c= Ut & xt in Vt ) by A1, A2;
hence Ut is a_neighborhood of xt by CONNSP_2:8; :: thesis: verum

end;

assume Ut is a_neighborhood of xt ; :: thesis: U is a_neighborhood of x
then consider Vt being Subset of (LinearTopSpaceNorm X) such that
A3: ( Vt is open & Vt c= Ut & xt in Vt ) by CONNSP_2:8;
reconsider V = Vt as open Subset of (TopSpaceNorm X) by A3, Def4, Th20;
( V is open & V c= U & x in V ) by A1, A3;
hence U is a_neighborhood of x by CONNSP_2:8; :: thesis: verum