for V being RealLinearSpace
for M being Subset of V
for r being Real st M is circled holds
r * M is circled