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 A1 is a_neighborhood of x1 & A = A1 & x = x1 holds
A is a_neighborhood of x

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 A1 is a_neighborhood of x1 & A = A1 & x = x1 holds
A is a_neighborhood of x

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 A1 is a_neighborhood of x1 & A = A1 & x = x1 holds
A is a_neighborhood of x

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

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

let x1 be Point of X; :: thesis: ( A1 is a_neighborhood of x1 & A = A1 & x = x1 implies A is a_neighborhood of x )
assume that
A1: A1 is a_neighborhood of x1 and
A2: A = A1 and
A3: x = x1 ; :: thesis: A is a_neighborhood of x
x1 in Int A1 by ;
then A4: x1 in (Int A1) /\ ([#] (X | B)) by ;
(Int A1) /\ ([#] (X | B)) c= Int A by ;
hence A is a_neighborhood of x by A3, A4, Def1; :: thesis: verum