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