let X be non empty TopSpace; :: thesis: for D being u.s.c._decomposition of X
for t being Point of (space D)
for G being a_neighborhood of (Proj D) " {t} holds (Proj D) .: G is a_neighborhood of t
let D be u.s.c._decomposition of X; :: thesis: for t being Point of (space D)
for G being a_neighborhood of (Proj D) " {t} holds (Proj D) .: G is a_neighborhood of t
let t be Point of (space D); :: thesis: for G being a_neighborhood of (Proj D) " {t} holds (Proj D) .: G is a_neighborhood of t
let G be a_neighborhood of (Proj D) " {t}; :: thesis: (Proj D) .: G is a_neighborhood of t
A1: the carrier of (space D) = D by Def10;
then (Proj D) " {t} = t by EQREL_1:66;
then consider W being Subset of X such that
A2: W is open and
A3: (Proj D) " {t} c= W and
A4: W c= G and
A5: for B being Subset of X st B in D & B meets W holds
B c= W by A1, Def13;
set Q = (Proj D) .: W;
A6: (Proj D) .: ((Proj D) " {t}) c= (Proj D) .: W by A3, RELAT_1:123;
union ((Proj D) .: W) = (proj D) " ((Proj D) .: W) by A1, EQREL_1:67
.= W by A5, EQREL_1:69 ;
then union ((Proj D) .: W) in the topology of X by A2, PRE_TOPC:def 2;
then (Proj D) .: W in the topology of (space D) by A1, Th69;
then A7: (Proj D) .: W is open by PRE_TOPC:def 2;
rng (Proj D) = the carrier of (space D) by Th72;
then {t} c= (Proj D) .: W by A6, FUNCT_1:77;
then A8: t in (Proj D) .: W by ZFMISC_1:31;
(Proj D) .: W c= (Proj D) .: G by A4, RELAT_1:123;
then t in Int ((Proj D) .: G) by A7, A8, TOPS_1:22;
hence (Proj D) .: G is a_neighborhood of t by CONNSP_2:def 1; :: thesis: verum