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'
p in Int Q by CONNSP_2:def 1;
then consider S being Subset of T such that
A2: ( S is open & S c= Q & p in S ) by TOPS_1:54;
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 A3: ( Q' = Q /\ P & p' = p ) ; :: thesis: Q' is a_neighborhood of p'
reconsider R = S /\ P as Subset of (T | P) by TOPS_2:38;
S /\ ([#] (T | P)) = S /\ P by PRE_TOPC:def 10;
then A4: R is open by A2, TOPS_2:32;
( R c= Q' & p' in R ) by A1, A2, A3, XBOOLE_0:def 4, XBOOLE_1:26;
then p' in Int Q' by A4, TOPS_1:54;
hence Q' is a_neighborhood of p' by CONNSP_2:def 1; :: thesis: verum