let X be RealNormSpace; :: thesis: for U being Subset of X
for Ut being Subset of ()
for x being Point of X
for xt being Point of () 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 ()
for x being Point of X
for xt being Point of () st U = Ut & x = xt holds
( U is Neighbourhood of x iff Ut is a_neighborhood of xt )

let Ut be Subset of (); :: thesis: for x being Point of X
for xt being Point of () 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 () st U = Ut & x = xt holds
( U is Neighbourhood of x iff Ut is a_neighborhood of xt )

let xt be Point of (); :: thesis: ( U = Ut & x = xt implies ( U is Neighbourhood of x iff Ut is a_neighborhood of xt ) )
assume that
A1: U = Ut and
A2: x = xt ; :: thesis: ( U is Neighbourhood of x iff Ut is a_neighborhood of xt )
A3: now :: thesis: ( U is Neighbourhood of x implies Ut is a_neighborhood of xt )
assume U is Neighbourhood of x ; :: thesis: Ut is a_neighborhood of xt
then consider r being Real such that
A4: r > 0 and
A5: { y where y is Point of X : ||.(y - x).|| < r } c= U by NFCONT_1:def 1;
now :: thesis: for s being object st s in { y where y is Point of X : ||.(y - x).|| < r } holds
s in the carrier of X
let s be object ; :: 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;
then reconsider Vt = { y where y is Point of X : ||.(y - x).|| < r } as Subset of () by TARSKI:def 3;
Vt = { y where y is Point of X : ||.(x - y).|| < r } by Lm5;
then A6: Vt is open by Th8;
||.(x - x).|| = 0 by NORMSP_1:6;
then xt in Vt by A2, A4;
hence Ut is a_neighborhood of xt by ; :: thesis: verum
end;
now :: thesis: ( Ut is a_neighborhood of xt implies U is Neighbourhood of x )
assume Ut is a_neighborhood of xt ; :: thesis: U is Neighbourhood of x
then consider Vt being Subset of () such that
A7: Vt is open and
A8: Vt c= Ut and
A9: xt in Vt by CONNSP_2:6;
consider r being Real such that
A10: r > 0 and
A11: { y where y is Point of X : ||.(x - y).|| < r } c= Vt by A2, A7, A9, Th7;
A12: { y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of X : ||.(y - x).|| < r } by Lm5;
{ y where y is Point of X : ||.(x - y).|| < r } c= U by A1, A8, A11;
hence U is Neighbourhood of x by ; :: thesis: verum
end;
hence ( U is Neighbourhood of x iff Ut is a_neighborhood of xt ) by A3; :: thesis: verum