let V be non empty CLSStruct ; :: thesis: for M being Subset of
for N being convex Subset of st M c= N holds
conv M c= N
let M be Subset of ; :: thesis: for N being convex Subset of st M c= N holds
conv M c= N
let N be convex Subset of ; :: 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:4; :: thesis: verum