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