theorem Th31: :: RLTOPSP1:31

for X being LinearTopSpace
for x1, x2 being Point of X
for V being a_neighborhood of x1 + x2 ex V1 being a_neighborhood of x1 ex V2 being a_neighborhood of x2 st V1 + V2 c= V