let X be LinearTopSpace; :: thesis: for x being Point of X
for V being a_neighborhood of x
for r being non zero Real holds r * V is a_neighborhood of r * x
let x be Point of X; :: thesis: for V being a_neighborhood of x
for r being non zero Real holds r * V is a_neighborhood of r * x
let V be a_neighborhood of x; :: thesis: for r being non zero Real holds r * V is a_neighborhood of r * x
let r be non zero Real; :: thesis: r * V is a_neighborhood of r * x
x in Int V by CONNSP_2:def 1;
then r * x in r * (Int V) ;
hence r * x in Int (r * V) by Th51; :: according to CONNSP_2:def 1 :: thesis: verum