defpred S₁[ Element of NAT ] means for i being Element of NAT st $1 <= i holds
not x. i in still_not-bound_in p;
{ k where k is Element of NAT : S₁[k] } c= NAT from FRAENKEL:sch 10();
hence { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p } is Subset of NAT ; :: thesis: verum