theorem Th20: :: QC_TRANS:20

for Al being QC-alphabet
for PHI being finite Subset of (CQC-WFF Al) ex Al1 being countable QC-alphabet st
( PHI is finite Subset of (CQC-WFF Al1) & Al is Al1 -expanding )