set f = + a;
for w being Point of G
for A being a_neighborhood of (+ a) . w ex W being a_neighborhood of w st (+ a) .: W c= A

let w be Point of G; :: thesis:
let A be a_neighborhood of (+ a) . w; :: thesis:
(+ a) . w = w + a by Def2;
then consider W being open a_neighborhood of w, B being open a_neighborhood of a such that
A3: W + B c= A by Th36;
take W ; :: thesis:
let k be object ; :: according to TARSKI:def 3 :: thesis:
assume k in (+ a) .: W ; :: thesis:
then k in W + a by Th16;
then A4: ex h being Element of G st
( k = h + a & h in W ) by Th28;
a in B by CONNSP_2:4;
then k in W + B by A4;
hence k in A by A3; :: thesis:

end;