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

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