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