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

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