theorem Th19: :: CQC_SIM1:19

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