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

let U be Subset of (); :: thesis: for Ut being Subset of
for x being Point of ()
for xt being Point of st U = Ut & x = xt holds
( U is a_neighborhood of x iff Ut is a_neighborhood of xt )

let Ut be Subset of ; :: thesis: for x being Point of ()
for xt being Point of st U = Ut & x = xt holds
( U is a_neighborhood of x iff Ut is a_neighborhood of xt )

let x be Point of (); :: thesis: for xt being Point of st U = Ut & x = xt holds
( U is a_neighborhood of x iff Ut is a_neighborhood of xt )

let xt be Point of ; :: thesis: ( U = Ut & x = xt implies ( U is a_neighborhood of x iff Ut is a_neighborhood of xt ) )
assume that
A1: U = Ut and
A2: 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 () such that
A3: V is open and
A4: V c= U and
A5: x in V by CONNSP_2:6;
reconsider Vt = V as open Subset of by ;
Vt c= Ut by A1, A4;
hence Ut is a_neighborhood of xt by ; :: thesis: verum
end;
assume Ut is a_neighborhood of xt ; :: thesis: U is a_neighborhood of x
then consider Vt being Subset of such that
A6: Vt is open and
A7: Vt c= Ut and
A8: xt in Vt by CONNSP_2:6;
reconsider V = Vt as open Subset of () by ;
V c= U by A1, A7;
hence U is a_neighborhood of x by ; :: thesis: verum