for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al holds
not for x being bound_QC-variable of Al holds x in still_not-bound_in f