A1: [:NAT,NAT:] is QC-alphabet by QC_LANG1:def 1;
[:NAT,NAT:] is countable by CARD_4:7;
hence ex b₁ being QC-alphabet st b₁ is countable by A1; :: thesis: verum