let V be RealLinearSpace; :: thesis: for M being circled Subset of V holds Cir M = M
let M be circled Subset of V; :: thesis: Cir M = M
thus Cir M c= M by Th12; :: according to XBOOLE_0:def 10 :: thesis: M c= Cir M
thus M c= Cir M by Th11; :: thesis: verum