let X be non empty TopSpace; :: thesis: TrivDecomp X is u.s.c._decomposition of X

thus for A being Subset of X st A in TrivDecomp X holds

for V being a_neighborhood of A ex W being Subset of X st

( W is open & A c= W & W c= V & ( for B being Subset of X st B in TrivDecomp X & B meets W holds

B c= W ) ) by Lm1; :: according to BORSUK_1:def 10 :: thesis: verum

thus for A being Subset of X st A in TrivDecomp X holds

for V being a_neighborhood of A ex W being Subset of X st

( W is open & A c= W & W c= V & ( for B being Subset of X st B in TrivDecomp X & B meets W holds

B c= W ) ) by Lm1; :: according to BORSUK_1:def 10 :: thesis: verum