let X be RealLinearSpace; :: thesis: for M being circled Subset of X holds conv M is circled
let M be circled Subset of X; :: thesis: conv M is circled
let r be Real; :: according to RLTOPSP1:def 6 :: thesis: ( |.r.| <= 1 implies r * (conv M) c= conv M )
assume |.r.| <= 1 ; :: thesis: r * (conv M) c= conv M
then A1: r * M c= M by Def6;
r * (conv M) = conv (r * M) by Th18;
hence r * (conv M) c= conv M by A1, Th20; :: thesis: verum