theorem Th12: :: QC_TRANS:12
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet
for p being Element of CQC-WFF Al holds still_not-bound_in p = still_not-bound_in (Al2 -Cast p)