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