theorem Th57: :: RLTOPSP1:57

for X being LinearTopSpace
for K being compact Subset of X
for C being closed Subset of X st K misses C holds
ex V being a_neighborhood of 0. X st K + V misses C + V