theorem :: CIRCLED1:5

for V being RealLinearSpace holds Up ((0). V) is circled