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
A1: (- x) + (Int V) = { ((- x) + v) where v is Point of X : v in Int V } by RUSUB_4:def 9;
A2: (- x) + (Int V) c= Int ((- x) + V) by Th38;
x in Int V by CONNSP_2:def 1;
then (- x) + x in (- x) + (Int V) by A1;
then 0. X in (- x) + (Int V) by RLVECT_1:16;
hence (- x) + V is a_neighborhood of 0. X by A2, CONNSP_2:def 1; :: thesis: verum