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 ;
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 ;
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 ;
then A8: Q /\ B is open by A1;
Q1 = Q /\ B by ;
then x1 in Int A1 by ;
hence A1 is a_neighborhood of x1 by Def1; :: thesis: verum