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