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

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