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 A1: A is finite ; :: thesis: not for x being bound_QC-variable holds x in A
not for b being set holds
( b in A iff b in bound_QC-variables ) by A1, CALCUL_1:64, TARSKI:2;
then consider b being set such that
A2: ( not b in A & 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 A2; :: thesis: verum