let A be Subset of XX; :: according to BORSUK_1:def 13 :: thesis:
assume A1: A in TrivExt D ; :: thesis:
let V be a_neighborhood of A; :: thesis:
A2: A c= Int V by CONNSP_2:def 2;
A3: Int V c= V by TOPS_1:44;

now

per cases by A1, Th74;

suppose A4: A in D ; :: thesis:

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

now

per cases by A12, Th74;

suppose A15: B in D ; :: thesis:

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

end;

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

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

end;

end;

end;

hence B c= H ; :: thesis:

end;

suppose A17: ex x being Point of XX st
( not x in [#] X & A = {x} ) ; :: thesis:

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

now

A22: W misses C by XBOOLE_1:79;
assume B in D ; :: thesis:
hence contradiction by A21, A22, XBOOLE_1:63; :: thesis:

end;

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

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: