let X be RealLinearSpace; :: thesis: for M1, M2 being Subset of X st M1 c= M2 holds
conv M1 c= conv M2
let M1, M2 be Subset of X; :: thesis: ( M1 c= M2 implies conv M1 c= conv M2 )
assume M1 c= M2 ; :: thesis: conv M1 c= conv M2
then Convex-Family M2 c= Convex-Family M1 by Th19;
then A1: meet (Convex-Family M1) c= meet (Convex-Family M2) by SETFAM_1:6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in conv M1 or x in conv M2 )
assume x in conv M1 ; :: thesis: x in conv M2
hence x in conv M2 by A1; :: thesis: verum