let A be Subset of bound_QC-variables; :: thesis: ( A is finite implies ex x being bound_QC-variable st not x in A )
assume A is finite ; :: thesis: not for x being bound_QC-variable holds x in A
then not for b being set holds
( b in A iff b in bound_QC-variables ) by CALCUL_1:64, TARSKI:2;
then consider b being set such that
A1: not b in A and
A2: b in bound_QC-variables ;
reconsider x = b as bound_QC-variable by A2;
take x ; :: thesis: not x in A
thus not x in A by A1; :: thesis: verum