let V be RealLinearSpace; :: thesis: for M being Subset of V
for N being circled Subset of V st M c= N holds
Cir M c= N
let M be Subset of V; :: thesis: for N being circled Subset of V st M c= N holds
Cir M c= N
let N be circled Subset of V; :: thesis: ( M c= N implies Cir M c= N )
assume M c= N ; :: thesis: Cir M c= N
then N in Circled-Family M by Def2;
hence Cir M c= N by SETFAM_1:3; :: thesis: verum