let V be RealLinearSpace; :: thesis: for M being Subset of V holds M c= conv M
let M be Subset of V; :: thesis: M c= conv M
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in M or v in conv M )
assume A1: v in M ; :: thesis: v in conv M
for Y being set st Y in Convex-Family M holds
v in Y

proof

let Y be set ; :: thesis: ( Y in Convex-Family M implies v in Y )
assume A2: Y in Convex-Family M ; :: thesis: v in Y
then reconsider Y = Y as Subset of V ;
M c= Y by A2, Def4;
hence v in Y by A1; :: thesis: verum

end;

hence v in conv M by SETFAM_1:def 1; :: thesis: verum