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