let X be LinearTopSpace; :: thesis: for x, v being Point of X
for V being a_neighborhood of x holds v + V is a_neighborhood of v + x
let x, v be Point of X; :: thesis: for V being a_neighborhood of x holds v + V is a_neighborhood of v + x
let V be a_neighborhood of x; :: thesis: v + V is a_neighborhood of v + x
( v + (Int V) = { (v + u) where u is Point of X : u in Int V } & x in Int V ) by CONNSP_2:def 1, RUSUB_4:def 8;
then A1: v + x in v + (Int V) ;
v + (Int V) = Int (v + V) by Th37;
hence v + V is a_neighborhood of v + x by A1, CONNSP_2:def 1; :: thesis: verum