QC-WFF is QC-closed by QC_LANG1:def 9;
then A1: QC-WFF is Subset of ([:NAT,NAT:] *) by QC_LANG1:def 8;
[:NAT,NAT:] is countable by CARD_4:7;
then [:NAT,NAT:] * is countable by CARD_4:13;
hence QC-WFF is countable by A1; :: thesis: verum