theorem Th19: :: QC_TRANS:19
for Al being QC-alphabet
for p being Element of CQC-WFF Al ex Al1 being countable QC-alphabet st
( p is Element of CQC-WFF Al1 & Al is Al1 -expanding )