let T be non empty TopSpace; :: thesis: for p being Point of T

for P being non empty Subset of T st p in P holds

for Q being a_neighborhood of p

for p9 being Point of (T | P)

for Q9 being Subset of (T | P) st Q9 = Q /\ P & p9 = p holds

Q9 is a_neighborhood of p9

let p be Point of T; :: thesis: for P being non empty Subset of T st p in P holds

for Q being a_neighborhood of p

for p9 being Point of (T | P)

for Q9 being Subset of (T | P) st Q9 = Q /\ P & p9 = p holds

Q9 is a_neighborhood of p9

let P be non empty Subset of T; :: thesis: ( p in P implies for Q being a_neighborhood of p

for p9 being Point of (T | P)

for Q9 being Subset of (T | P) st Q9 = Q /\ P & p9 = p holds

Q9 is a_neighborhood of p9 )

assume A1: p in P ; :: thesis: for Q being a_neighborhood of p

for p9 being Point of (T | P)

for Q9 being Subset of (T | P) st Q9 = Q /\ P & p9 = p holds

Q9 is a_neighborhood of p9

let Q be a_neighborhood of p; :: thesis: for p9 being Point of (T | P)

for Q9 being Subset of (T | P) st Q9 = Q /\ P & p9 = p holds

Q9 is a_neighborhood of p9

let p9 be Point of (T | P); :: thesis: for Q9 being Subset of (T | P) st Q9 = Q /\ P & p9 = p holds

Q9 is a_neighborhood of p9

let Q9 be Subset of (T | P); :: thesis: ( Q9 = Q /\ P & p9 = p implies Q9 is a_neighborhood of p9 )

assume that

A2: Q9 = Q /\ P and

A3: p9 = p ; :: thesis: Q9 is a_neighborhood of p9

p in Int Q by CONNSP_2:def 1;

then consider S being Subset of T such that

A4: S is open and

A5: S c= Q and

A6: p in S by TOPS_1:22;

reconsider R = S /\ P as Subset of (T | P) by TOPS_2:29;

A7: R c= Q9 by A5, A2, XBOOLE_1:26;

S /\ ([#] (T | P)) = S /\ P by PRE_TOPC:def 5;

then A8: R is open by A4, TOPS_2:24;

p9 in R by A1, A6, A3, XBOOLE_0:def 4;

then p9 in Int Q9 by A8, A7, TOPS_1:22;

hence Q9 is a_neighborhood of p9 by CONNSP_2:def 1; :: thesis: verum

for P being non empty Subset of T st p in P holds

for Q being a_neighborhood of p

for p9 being Point of (T | P)

for Q9 being Subset of (T | P) st Q9 = Q /\ P & p9 = p holds

Q9 is a_neighborhood of p9

let p be Point of T; :: thesis: for P being non empty Subset of T st p in P holds

for Q being a_neighborhood of p

for p9 being Point of (T | P)

for Q9 being Subset of (T | P) st Q9 = Q /\ P & p9 = p holds

Q9 is a_neighborhood of p9

let P be non empty Subset of T; :: thesis: ( p in P implies for Q being a_neighborhood of p

for p9 being Point of (T | P)

for Q9 being Subset of (T | P) st Q9 = Q /\ P & p9 = p holds

Q9 is a_neighborhood of p9 )

assume A1: p in P ; :: thesis: for Q being a_neighborhood of p

for p9 being Point of (T | P)

for Q9 being Subset of (T | P) st Q9 = Q /\ P & p9 = p holds

Q9 is a_neighborhood of p9

let Q be a_neighborhood of p; :: thesis: for p9 being Point of (T | P)

for Q9 being Subset of (T | P) st Q9 = Q /\ P & p9 = p holds

Q9 is a_neighborhood of p9

let p9 be Point of (T | P); :: thesis: for Q9 being Subset of (T | P) st Q9 = Q /\ P & p9 = p holds

Q9 is a_neighborhood of p9

let Q9 be Subset of (T | P); :: thesis: ( Q9 = Q /\ P & p9 = p implies Q9 is a_neighborhood of p9 )

assume that

A2: Q9 = Q /\ P and

A3: p9 = p ; :: thesis: Q9 is a_neighborhood of p9

p in Int Q by CONNSP_2:def 1;

then consider S being Subset of T such that

A4: S is open and

A5: S c= Q and

A6: p in S by TOPS_1:22;

reconsider R = S /\ P as Subset of (T | P) by TOPS_2:29;

A7: R c= Q9 by A5, A2, XBOOLE_1:26;

S /\ ([#] (T | P)) = S /\ P by PRE_TOPC:def 5;

then A8: R is open by A4, TOPS_2:24;

p9 in R by A1, A6, A3, XBOOLE_0:def 4;

then p9 in Int Q9 by A8, A7, TOPS_1:22;

hence Q9 is a_neighborhood of p9 by CONNSP_2:def 1; :: thesis: verum