theorem Th16: :: CIRCLED1:16

for V being RealLinearSpace
for L being Linear_Combination of V st L is circled holds
Carrier L <> {}