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

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