theorem Th32: :: RLTOPSP1:32

for X being LinearTopSpace
for a being Real
for x being Point of X
for V being a_neighborhood of a * x ex r being positive Real ex W being a_neighborhood of x st
for s being Real st |.(s - a).| < r holds
s * W c= V