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

A2: now

assume Ut is a_neighborhood of xt ; :: thesis: U is Neighbourhood of x
then consider Vt being Subset of (TopSpaceNorm X) such that
A3: ( Vt is open & Vt c= Ut & xt in Vt ) by CONNSP_2:8;
consider r being Real such that
A4: ( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= Vt ) by A1, A3, Th7;
A5: { y where y is Point of X : ||.(x - y).|| < r } c= U by A1, A3, A4, XBOOLE_1:1;
{ y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of X : ||.(y - x).|| < r } by Lm5;
hence U is Neighbourhood of x by A4, A5, NFCONT_1:def 3; :: thesis: verum

end;

now

assume U is Neighbourhood of x ; :: thesis: Ut is a_neighborhood of xt
then consider r being Real such that
A6: ( r > 0 & { y where y is Point of X : ||.(y - x).|| < r } c= U ) by NFCONT_1:def 3;
{ y where y is Point of X : ||.(y - x).|| < r } c= the carrier of X

proof

now

let s be set ; :: thesis: ( s in { y where y is Point of X : ||.(y - x).|| < r } implies s in the carrier of X )
assume s in { y where y is Point of X : ||.(y - x).|| < r } ; :: thesis: s in the carrier of X
then ex z being Point of X st
( s = z & ||.(z - x).|| < r ) ;
hence s in the carrier of X ; :: thesis: verum

end;

hence { y where y is Point of X : ||.(y - x).|| < r } c= the carrier of X by TARSKI:def 3; :: thesis: verum

end;

then reconsider Vt = { y where y is Point of X : ||.(y - x).|| < r } as Subset of (TopSpaceNorm X) ;
Vt = { y where y is Point of X : ||.(x - y).|| < r } by Lm5;
then A7: Vt is open by Th8;
||.(x - x).|| = 0 by NORMSP_1:10;
then xt in Vt by A1, A6;
hence Ut is a_neighborhood of xt by A1, A6, A7, CONNSP_2:8; :: thesis: verum

end;

hence ( U is Neighbourhood of x iff Ut is a_neighborhood of xt ) by A2; :: thesis: verum