defpred S_{1}[ Subset of V] means ( $1 is convex & M c= $1 );

thus ex F being Subset-Family of V st

for N being Subset of V holds

( N in F iff S_{1}[N] )
from SUBSET_1:sch 3(); :: thesis: verum

thus ex F being Subset-Family of V st

for N being Subset of V holds

( N in F iff S