let X be non empty TopSpace; :: thesis: for B being non empty Subset of X

for x being Point of (X | B)

for A being Subset of (X | B)

for A1 being Subset of X

for x1 being Point of X st B is open & A is a_neighborhood of x & A = A1 & x = x1 holds

A1 is a_neighborhood of x1

let B be non empty Subset of X; :: thesis: for x being Point of (X | B)

for A being Subset of (X | B)

for A1 being Subset of X

for x1 being Point of X st B is open & A is a_neighborhood of x & A = A1 & x = x1 holds

A1 is a_neighborhood of x1

let x be Point of (X | B); :: thesis: for A being Subset of (X | B)

for A1 being Subset of X

for x1 being Point of X st B is open & A is a_neighborhood of x & A = A1 & x = x1 holds

A1 is a_neighborhood of x1

let A be Subset of (X | B); :: thesis: for A1 being Subset of X

for x1 being Point of X st B is open & A is a_neighborhood of x & A = A1 & x = x1 holds

A1 is a_neighborhood of x1

let A1 be Subset of X; :: thesis: for x1 being Point of X st B is open & A is a_neighborhood of x & A = A1 & x = x1 holds

A1 is a_neighborhood of x1

let x1 be Point of X; :: thesis: ( B is open & A is a_neighborhood of x & A = A1 & x = x1 implies A1 is a_neighborhood of x1 )

assume that

A1: B is open and

A2: A is a_neighborhood of x and

A3: ( A = A1 & x = x1 ) ; :: thesis: A1 is a_neighborhood of x1

x in Int A by A2, Def1;

then consider Q1 being Subset of (X | B) such that

A4: Q1 is open and

A5: ( Q1 c= A & x in Q1 ) by TOPS_1:22;

Q1 in the topology of (X | B) by A4, PRE_TOPC:def 2;

then consider Q being Subset of X such that

A6: Q in the topology of X and

A7: Q1 = Q /\ ([#] (X | B)) by PRE_TOPC:def 4;

reconsider Q2 = Q as Subset of X ;

Q2 is open by A6, PRE_TOPC:def 2;

then A8: Q /\ B is open by A1;

Q1 = Q /\ B by A7, PRE_TOPC:def 5;

then x1 in Int A1 by A3, A5, A8, TOPS_1:22;

hence A1 is a_neighborhood of x1 by Def1; :: thesis: verum

for x being Point of (X | B)

for A being Subset of (X | B)

for A1 being Subset of X

for x1 being Point of X st B is open & A is a_neighborhood of x & A = A1 & x = x1 holds

A1 is a_neighborhood of x1

let B be non empty Subset of X; :: thesis: for x being Point of (X | B)

for A being Subset of (X | B)

for A1 being Subset of X

for x1 being Point of X st B is open & A is a_neighborhood of x & A = A1 & x = x1 holds

A1 is a_neighborhood of x1

let x be Point of (X | B); :: thesis: for A being Subset of (X | B)

for A1 being Subset of X

for x1 being Point of X st B is open & A is a_neighborhood of x & A = A1 & x = x1 holds

A1 is a_neighborhood of x1

let A be Subset of (X | B); :: thesis: for A1 being Subset of X

for x1 being Point of X st B is open & A is a_neighborhood of x & A = A1 & x = x1 holds

A1 is a_neighborhood of x1

let A1 be Subset of X; :: thesis: for x1 being Point of X st B is open & A is a_neighborhood of x & A = A1 & x = x1 holds

A1 is a_neighborhood of x1

let x1 be Point of X; :: thesis: ( B is open & A is a_neighborhood of x & A = A1 & x = x1 implies A1 is a_neighborhood of x1 )

assume that

A1: B is open and

A2: A is a_neighborhood of x and

A3: ( A = A1 & x = x1 ) ; :: thesis: A1 is a_neighborhood of x1

x in Int A by A2, Def1;

then consider Q1 being Subset of (X | B) such that

A4: Q1 is open and

A5: ( Q1 c= A & x in Q1 ) by TOPS_1:22;

Q1 in the topology of (X | B) by A4, PRE_TOPC:def 2;

then consider Q being Subset of X such that

A6: Q in the topology of X and

A7: Q1 = Q /\ ([#] (X | B)) by PRE_TOPC:def 4;

reconsider Q2 = Q as Subset of X ;

Q2 is open by A6, PRE_TOPC:def 2;

then A8: Q /\ B is open by A1;

Q1 = Q /\ B by A7, PRE_TOPC:def 5;

then x1 in Int A1 by A3, A5, A8, TOPS_1:22;

hence A1 is a_neighborhood of x1 by Def1; :: thesis: verum