defpred S₁[ Subset of ] means ( $1 is convex & M c= $1 );
thus ex F being Subset-Family of st
for N being Subset of holds
( N in F iff S₁[N] ) from SUBSET_1:sch 3(); :: thesis: verum