let X be non empty TopSpace; :: thesis: for A being Subset of X
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 ) )
let A be Subset of X; :: thesis: 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 ) )
let V be a_neighborhood of A; :: thesis: 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 ) )
take Int V ; :: thesis: ( Int V is open & A c= Int V & Int V c= V & ( for B being Subset of X st B in TrivDecomp X & B meets Int V holds
B c= Int V ) )
thus Int V is open ; :: thesis: ( A c= Int V & Int V c= V & ( for B being Subset of X st B in TrivDecomp X & B meets Int V holds
B c= Int V ) )
thus A c= Int V by CONNSP_2:def 2; :: thesis: ( Int V c= V & ( for B being Subset of X st B in TrivDecomp X & B meets Int V holds
B c= Int V ) )
thus Int V c= V by TOPS_1:16; :: thesis: for B being Subset of X st B in TrivDecomp X & B meets Int V holds
B c= Int V
let B be Subset of X; :: thesis: ( B in TrivDecomp X & B meets Int V implies B c= Int V )
assume that
A1: B in TrivDecomp X and
A2: B meets Int V ; :: thesis: B c= Int V
consider x being Point of X such that
A3: B = {x} by A1, Th26;
x in Int V by A2, A3, ZFMISC_1:50;
hence B c= Int V by A3, ZFMISC_1:31; :: thesis: verum