let Al be QC-alphabet ; :: thesis: ( Al is countable implies QC-WFF Al is countable )
assume A1: Al is countable ; :: thesis: QC-WFF Al is countable
QC-WFF Al is Al -closed by QC_LANG1:def 11;
then A2: QC-WFF Al is Subset of ([:NAT,(QC-symbols Al):] *) by QC_LANG1:def 10;
( [:NAT,(QC-symbols Al):] is non empty set & [:NAT,(QC-symbols Al):] is countable ) by A1, QC_LANG1:5;
then [:NAT,(QC-symbols Al):] * is countable by CARD_4:13;
hence QC-WFF Al is countable by A2; :: thesis: verum