let Al be QC-alphabet ; :: thesis: for f being FinSequence of CQC-WFF Al holds
not for x being bound_QC-variable of Al holds x in still_not-bound_in f
let f be FinSequence of CQC-WFF Al; :: thesis: not for x being bound_QC-variable of Al holds x in still_not-bound_in f
still_not-bound_in f is finite by Th62;
then still_not-bound_in f <> bound_QC-variables Al by Th63;
then not for b being object holds
( b in still_not-bound_in f iff b in bound_QC-variables Al ) by TARSKI:2;
then consider b being object such that
A1: not b in still_not-bound_in f and
A2: b in bound_QC-variables Al ;
reconsider x = b as bound_QC-variable of Al by A2;
take x ; :: thesis: not x in still_not-bound_in f
thus not x in still_not-bound_in f by A1; :: thesis: verum