let X be RealLinearSpace; :: thesis: conv ({} X) = {}
{} X is convex ;
then {} X in Convex-Family ({} X) by CONVEX1:def 4;
hence conv ({} X) = {} by SETFAM_1:4; :: thesis: verum