theorem :: CIRCLED1:13

for V being RealLinearSpace
for M being circled Subset of V holds Cir M = M by Th12, Th11;