defpred S₁[ set ] means $1 is finite ;
{ p where p is Element of sproduct the Object-Kind of S : S₁[p] } c= sproduct the Object-Kind of S from FRAENKEL:sch 10();
hence { p where p is Element of sproduct the Object-Kind of S : p is finite } is Subset of (sproduct the Object-Kind of S) ; :: thesis: verum