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 Def7;

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, Def10;

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;

then (Proj D) .: W in the topology of (space D) by A1, Th27;

then A7: (Proj D) .: W is open ;

rng (Proj D) = the carrier of (space D) by Th30;

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

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 Def7;

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, Def10;

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;

then (Proj D) .: W in the topology of (space D) by A1, Th27;

then A7: (Proj D) .: W is open ;

rng (Proj D) = the carrier of (space D) by Th30;

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