theorem Th12: :: QC_TRANS:12

for Al being QC-alphabet
for Al2 being b₁ -expanding QC-alphabet
for p being Element of CQC-WFF Al holds still_not-bound_in p = still_not-bound_in (Al2 -Cast p)