take TrivDecomp X ; :: thesis: 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 ) )
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; :: thesis: verum