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

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

hence
v in conv M
by SETFAM_1:def 1; :: thesis: verum
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;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