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

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