card bound_QC-variables = card [:NAT ,{4}:] by CARD_2:11, QC_LANG1:def 2;
then card bound_QC-variables = omega by CARD_1:84, CARD_4:81;
hence ( card bound_QC-variables = omega & not bound_QC-variables is finite ) ; :: thesis: verum