defpred S₁[ set ] means $1 is finite ;
thus ex W being Subset of X st
for x being set holds
( x in W iff ( x in X & S₁[x] ) ) from SUBSET_1:sch 1(); :: thesis: verum