let A be Subset of XX; :: according to BORSUK_1:def 10 :: 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: A c= Int V by CONNSP_2:def 2;

A3: Int V c= V by TOPS_1:16;

( 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

( 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: A c= Int V by CONNSP_2:def 2;

A3: Int V c= V by TOPS_1:16;

now :: 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 ) )end;

hence
ex W being Subset 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 ) )

per cases
( A in D or ex x being Point of XX st

( not x in [#] X & A = {x} ) ) by A1, Th31;

end;

( not x in [#] X & A = {x} ) ) by A1, Th31;

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 ) )

( 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 ;

( E is open & C c= E ) by A2, TOPS_2:24, XBOOLE_1:19;

then C c= Int E by TOPS_1:23;

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, Def10;

consider G being Subset of XX such that

A9: G is open and

A10: W = G /\ ([#] X) by A5, TOPS_2:24;

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; :: 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 A6;

hence A c= H by A2, 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 A3; :: thesis: for B being Subset of XX st B in TrivExt D & B meets H holds

B c= H

let B be Subset of XX; :: thesis: ( B in TrivExt D & B meets H implies B c= H )

assume that

A12: B in TrivExt D and

A13: B meets H ; :: thesis: B c= H

E c= Int V by XBOOLE_1:17;

then W c= Int V by A7;

then A14: W c= H by A11, XBOOLE_1:19;

end;reconsider E = (Int V) /\ ([#] X) as Subset of X ;

( E is open & C c= E ) by A2, TOPS_2:24, XBOOLE_1:19;

then C c= Int E by TOPS_1:23;

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, Def10;

consider G being Subset of XX such that

A9: G is open and

A10: W = G /\ ([#] X) by A5, TOPS_2:24;

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; :: 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 A6;

hence A c= H by A2, 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 A3; :: thesis: for B being Subset of XX st B in TrivExt D & B meets H holds

B c= H

let B be Subset of XX; :: thesis: ( B in TrivExt D & B meets H implies B c= H )

assume that

A12: B in TrivExt D and

A13: B meets H ; :: thesis: B c= H

E c= Int V by XBOOLE_1:17;

then W c= Int V by A7;

then A14: W c= H by A11, XBOOLE_1:19;

now :: thesis: B c= H

hence
B c= H
; :: thesis: verumend;

suppose A17:
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 ) )

( 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 ) )

[#] X c= [#] XX
by PRE_TOPC:def 4;

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 Def11;

then (Int V) /\ (C `) is open ;

hence W is open by SUBSET_1:13; :: 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 ) )

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:31; :: 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 A3; :: 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 that

A20: B in TrivExt D and

A21: B meets W ; :: thesis: B c= W

not y in [#] X and

A23: B = {y} by A20, Th31;

y in W by A21, A23, ZFMISC_1:50;

hence B c= W by A23, ZFMISC_1:31; :: thesis: verum

end;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 Def11;

then (Int V) /\ (C `) is open ;

hence W is open by SUBSET_1:13; :: 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 ) )

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:31; :: 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 A3; :: 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 that

A20: B in TrivExt D and

A21: B meets W ; :: thesis: B c= W

now :: thesis: not B in D

then consider y being Point of XX such that A22:
W misses C
by XBOOLE_1:79;

assume B in D ; :: thesis: contradiction

hence contradiction by A21, A22, XBOOLE_1:63; :: thesis: verum

end;assume B in D ; :: thesis: contradiction

hence contradiction by A21, A22, XBOOLE_1:63; :: thesis: verum

not y in [#] X and

A23: B = {y} by A20, Th31;

y in W by A21, A23, ZFMISC_1:50;

hence B c= W by A23, ZFMISC_1:31; :: thesis: verum

( 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