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