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

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