let X be RealLinearSpace; :: thesis: for M1, M2 being Subset of X st M1 c= M2 holds
Convex-Family M2 c= Convex-Family M1
let M1, M2 be Subset of X; :: thesis: ( M1 c= M2 implies Convex-Family M2 c= Convex-Family M1 )
assume A1: M1 c= M2 ; :: thesis: Convex-Family M2 c= Convex-Family M1
let M be object ; :: according to TARSKI:def 3 :: thesis: ( not M in Convex-Family M2 or M in Convex-Family M1 )
assume A2: M in Convex-Family M2 ; :: thesis: M in Convex-Family M1
then reconsider M = M as Subset of X ;
M2 c= M by A2, CONVEX1:def 4;
then A3: M1 c= M by A1;
M is convex by A2, CONVEX1:def 4;
hence M in Convex-Family M1 by A3, CONVEX1:def 4; :: thesis: verum