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