:: deftheorem Def4 defines Convex-Family CONVEX1:def 4 :
for V being non empty RLSStruct
for M being Subset of V
for b₃ being Subset-Family of V holds
( b₃ = Convex-Family M iff for N being Subset of V holds
( N in b₃ iff ( N is convex & M c= N ) ) );