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