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 p' being Point of (T | P)
for Q' being Subset of (T | P) st Q' = Q /\ P & p' = p holds
Q' is a_neighborhood of p'
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 p' being Point of (T | P)
for Q' being Subset of (T | P) st Q' = Q /\ P & p' = p holds
Q' is a_neighborhood of p'
let P be non empty Subset of T; :: thesis: ( p in P implies for Q being a_neighborhood of p
for p' being Point of (T | P)
for Q' being Subset of (T | P) st Q' = Q /\ P & p' = p holds
Q' is a_neighborhood of p' )
assume A1: p in P ; :: thesis: for Q being a_neighborhood of p
for p' being Point of (T | P)
for Q' being Subset of (T | P) st Q' = Q /\ P & p' = p holds
Q' is a_neighborhood of p'
let Q be a_neighborhood of p; :: thesis: for p' being Point of (T | P)
for Q' being Subset of (T | P) st Q' = Q /\ P & p' = p holds
Q' is a_neighborhood of p'
let p' be Point of (T | P); :: thesis: for Q' being Subset of (T | P) st Q' = Q /\ P & p' = p holds
Q' is a_neighborhood of p'
let Q' be Subset of (T | P); :: thesis: ( Q' = Q /\ P & p' = p implies Q' is a_neighborhood of p' )
assume that
A2: Q' = Q /\ P and
A3: p' = p ; :: thesis: Q' is a_neighborhood of p'
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:54;
reconsider R = S /\ P as Subset of (T | P) by TOPS_2:38;
A7: R c= Q' by A5, A2, XBOOLE_1:26;
S /\ ([#] (T | P)) = S /\ P by PRE_TOPC:def 10;
then A8: R is open by A4, TOPS_2:32;
p' in R by A1, A6, A3, XBOOLE_0:def 4;
then p' in Int Q' by A8, A7, TOPS_1:54;
hence Q' is a_neighborhood of p' by CONNSP_2:def 1; :: thesis: verum