:: deftheorem defines conv CONVEX1:def 5 :
for V being non empty RLSStruct
for M being Subset of V holds conv M = meet (Convex-Family M);