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