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 A1, Def1;
then A4: x1 in (Int A1) /\ ([#] (X | B)) by A3, XBOOLE_0:def 4;
(Int A1) /\ ([#] (X | B)) c= Int A by A2, Lm1;
hence A is a_neighborhood of x by A3, A4, Def1; :: thesis: verum