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 that

A1: U = Ut and

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

then consider Vt being Subset of (LinearTopSpaceNorm X) 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 (TopSpaceNorm X) by A6, Def4, Th20;

V c= U by A1, A7;

hence U is a_neighborhood of x by A2, A8, CONNSP_2:6; :: thesis: verum

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 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
Ut is a_neighborhood of xt
; :: thesis: U is a_neighborhood of xassume
U is a_neighborhood of x
; :: thesis: Ut is a_neighborhood of xt

then consider V being Subset of (TopSpaceNorm X) 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 (LinearTopSpaceNorm X) by A3, Def4, Th20;

Vt c= Ut by A1, A4;

hence Ut is a_neighborhood of xt by A2, A5, CONNSP_2:6; :: thesis: verum

end;then consider V being Subset of (TopSpaceNorm X) 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 (LinearTopSpaceNorm X) by A3, Def4, Th20;

Vt c= Ut by A1, A4;

hence Ut is a_neighborhood of xt by A2, A5, CONNSP_2:6; :: thesis: verum

then consider Vt being Subset of (LinearTopSpaceNorm X) 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 (TopSpaceNorm X) by A6, Def4, Th20;

V c= U by A1, A7;

hence U is a_neighborhood of x by A2, A8, CONNSP_2:6; :: thesis: verum