let X be RealLinearSpace; :: thesis: for M being convex Subset of X holds conv M = M
let M be convex Subset of X; :: thesis: conv M = M
thus conv M c= M by CONVEX1:30; :: according to XBOOLE_0:def 10 :: thesis: M c= conv M
thus M c= conv M by CONVEX1:41; :: thesis: verum