let Al be QC-alphabet ; :: thesis: ( Al is countable implies CQC-WFF Al is countable )
assume A1: Al is countable ; :: thesis: CQC-WFF Al is countable
QC-WFF Al is countable by Th18, A1;
hence CQC-WFF Al is countable ; :: thesis: verum