let V be non empty CLSStruct ; :: thesis: for M being Subset of V
for N being convex Subset of V st M c= N holds
conv M c= N
let M be Subset of V; :: thesis: for N being convex Subset of V st M c= N holds
conv M c= N
let N be convex Subset of V; :: thesis: ( M c= N implies conv M c= N )
assume M c= N ; :: thesis: conv M c= N
then N in Convex-Family M by Def25;
hence conv M c= N by SETFAM_1:3; :: thesis: verum