let Al be QC-alphabet ; :: thesis: ( card (bound_QC-variables Al) = card (QC-symbols Al) & not bound_QC-variables Al is finite )
NAT c= QC-symbols Al by QC_LANG1:3;
then A1: not QC-symbols Al is finite ;
bound_QC-variables Al = [:{4},(QC-symbols Al):] by QC_LANG1:def 4;
then card (bound_QC-variables Al) = card [:(QC-symbols Al),{4}:] by CARD_2:4;
hence ( card (bound_QC-variables Al) = card (QC-symbols Al) & not bound_QC-variables Al is finite ) by A1, CARD_4:19; :: thesis: verum