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 that

A1: U = Ut and

A2: x = xt ; :: thesis: ( U is Neighbourhood of x iff Ut is a_neighborhood of xt )

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 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;

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 A1, A5, A6, CONNSP_2:6; :: thesis: verum

end;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

then reconsider Vt = { y where y is Point of X : ||.(y - x).|| < r } as Subset of (TopSpaceNorm X) by TARSKI:def 3;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;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

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 A1, A5, A6, CONNSP_2:6; :: thesis: verum

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

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

then consider Vt being Subset of (TopSpaceNorm X) 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 A10, A12, NFCONT_1:def 1; :: thesis: verum

end;then consider Vt being Subset of (TopSpaceNorm X) 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 A10, A12, NFCONT_1:def 1; :: thesis: verum