let V be non empty RLSStruct ; :: 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 Def4;

hence conv M c= N by SETFAM_1:3; :: thesis: verum

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 Def4;

hence conv M c= N by SETFAM_1:3; :: thesis: verum