let X, Y be non empty TopSpace; :: thesis: for W being Point of Y
for A being continuous Function of X,Y
for G being a_neighborhood of W holds A " G is a_neighborhood of A " {W}

let W be Point of Y; :: thesis: for A being continuous Function of X,Y
for G being a_neighborhood of W holds A " G is a_neighborhood of A " {W}

let A be continuous Function of X,Y; :: thesis: for G being a_neighborhood of W holds A " G is a_neighborhood of A " {W}
let G be a_neighborhood of W; :: thesis: A " G is a_neighborhood of A " {W}
W in Int G by CONNSP_2:def 1;
then {W} c= Int G by ZFMISC_1:31;
then A1: A " {W} c= A " (Int G) by RELAT_1:143;
A " (Int G) c= Int (A " G) by Th2;
hence A " {W} c= Int (A " G) by A1; :: according to CONNSP_2:def 2 :: thesis: verum