for A being QC-alphabet
for p being Element of QC-WFF A holds still_not-bound_in p is finite