let W be Point of X; :: according to BORSUK_1:def 1 :: thesis: for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G
let G be a_neighborhood of F . W; :: thesis: ex H being a_neighborhood of W st F .: H c= G
reconsider H = union (Int G) as Subset of X by A1, EQREL_1:61;
F . W in Int G by CONNSP_2:def 1;
then W in F " (Int G) by FUNCT_2:38;
then A2: W in union (Int G) by A1, EQREL_1:67;
Int G in the topology of (space D) by PRE_TOPC:def 2;
then union (Int G) in the topology of X by A1, Th27;
then H is open ;
then W in Int H by A2, TOPS_1:23;
then W in Int (F " (Int G)) by A1, EQREL_1:67;
then reconsider N = F " (Int G) as a_neighborhood of W by CONNSP_2:def 1;
take N ; :: thesis: F .: N c= G
( F .: N c= Int G & Int G c= G ) by FUNCT_1:75, TOPS_1:16;
hence F .: N c= G ; :: thesis: verum