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 ;
S /\ ([#] (T | P)) = S /\ P by PRE_TOPC:def 5;
then A8: R is open by ;
p9 in R by ;
then p9 in Int Q9 by ;
hence Q9 is a_neighborhood of p9 by CONNSP_2:def 1; :: thesis: verum