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