let A be Subset of XX; :: according to BORSUK_1:def 13 :: thesis: ( A in TrivExt D implies for V being a_neighborhood of A ex W being Subset of XX st
( W is open & A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) ) )
assume A1: A in TrivExt D ; :: thesis: for V being a_neighborhood of A ex W being Subset of XX st
( W is open & A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) )
let V be a_neighborhood of A; :: thesis: ex W being Subset of XX st
( W is open & A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) )
A2: Int V c= V by TOPS_1:44;
A3: A c= Int V by CONNSP_2:def 2;

now

per cases ( A in D or ex x being Point of XX st
( not x in [#] X & A = {x} ) ) by A1, Th74;

suppose A4: A in D ; :: thesis: ex H being Element of bool the carrier of XX st
( H is open & A c= H & H c= V & ( for B being Subset of XX st B in TrivExt D & B meets H holds
B c= H ) )

then reconsider C = A as Subset of X ;
reconsider E = (Int V) /\ ([#] X) as Subset of X ;
A5: E is open by TOPS_2:32;
C c= E by A3, XBOOLE_1:19;
then C c= Int E by A5, TOPS_1:55;
then E is a_neighborhood of C by CONNSP_2:def 2;
then consider W being Subset of X such that
A6: W is open and
A7: ( C c= W & W c= E ) and
A8: for B being Subset of X st B in D & B meets W holds
B c= W by A4, Def13;
consider G being Subset of XX such that
A9: G is open and
A10: W = G /\ ([#] X) by A6, TOPS_2:32;
take H = G /\ (Int V); :: thesis: ( H is open & A c= H & H c= V & ( for B being Subset of XX st B in TrivExt D & B meets H holds
B c= H ) )
thus H is open by A9, TOPS_1:38; :: thesis: ( A c= H & H c= V & ( for B being Subset of XX st B in TrivExt D & B meets H holds
B c= H ) )
A11: W c= G by A10, XBOOLE_1:17;
then C c= G by A7, XBOOLE_1:1;
hence A c= H by A3, XBOOLE_1:19; :: thesis: ( H c= V & ( for B being Subset of XX st B in TrivExt D & B meets H holds
B c= H ) )
H c= Int V by XBOOLE_1:17;
hence H c= V by A2, XBOOLE_1:1; :: thesis: for B being Subset of XX st B in TrivExt D & B meets H holds
B c= H
E c= Int V by XBOOLE_1:17;
then W c= Int V by A7, XBOOLE_1:1;
then A12: W c= H by A11, XBOOLE_1:19;
let B be Subset of XX; :: thesis: ( B in TrivExt D & B meets H implies B c= H )
assume A13: ( B in TrivExt D & B meets H ) ; :: thesis: B c= H

now

per cases ( B in D or ex y being Point of XX st
( not y in [#] X & B = {y} ) ) by A13, Th74;

suppose A14: B in D ; :: thesis: B c= H

B meets G by A13, XBOOLE_1:74;
then B meets W by A10, A14, XBOOLE_1:77;
then B c= W by A8, A14;
hence B c= H by A12, XBOOLE_1:1; :: thesis: verum

end;

suppose ex y being Point of XX st
( not y in [#] X & B = {y} ) ; :: thesis: B c= H

then consider y being Point of XX such that
A15: ( not y in [#] X & B = {y} ) ;
y in H by A13, A15, ZFMISC_1:56;
hence B c= H by A15, ZFMISC_1:37; :: thesis: verum

end;

end;

end;

hence B c= H ; :: thesis: verum

end;

suppose ex x being Point of XX st
( not x in [#] X & A = {x} ) ; :: thesis: ex W being Element of bool the carrier of XX st
( W is open & A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) )

then consider x being Point of XX such that
A16: not x in [#] X and
A17: A = {x} ;
[#] X c= [#] XX by PRE_TOPC:def 9;
then reconsider C = [#] X as Subset of XX ;
take W = (Int V) \ C; :: thesis: ( W is open & A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) )
C is closed by Def14;
then (Int V) /\ (C ` ) is open by TOPS_1:38;
hence W is open by SUBSET_1:32; :: thesis: ( A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) )
x in A by A17, TARSKI:def 1;
then x in W by A3, A16, XBOOLE_0:def 5;
hence A c= W by A17, ZFMISC_1:37; :: thesis: ( W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) )
W c= Int V by XBOOLE_1:36;
hence W c= V by A2, XBOOLE_1:1; :: thesis: for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W
let B be Subset of XX; :: thesis: ( B in TrivExt D & B meets W implies B c= W )
assume A18: ( B in TrivExt D & B meets W ) ; :: thesis: B c= W

now

assume A19: B in D ; :: thesis: contradiction
W misses C by XBOOLE_1:79;
hence contradiction by A18, A19, XBOOLE_1:63; :: thesis: verum

end;

then consider y being Point of XX such that
not y in [#] X and
A20: B = {y} by A18, Th74;
y in W by A18, A20, ZFMISC_1:56;
hence B c= W by A20, ZFMISC_1:37; :: thesis: verum

end;

end;

end;

hence ex W being Subset of XX st
( W is open & A c= W & W c= V & ( for B being Subset of XX st B in TrivExt D & B meets W holds
B c= W ) ) ; :: thesis: verum