theorem Th7: :: QC_TRANS:7
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet
for p being Element of CQC-WFF Al holds p is Element of CQC-WFF Al2