let f be FinSequence of CQC-WFF ; :: thesis: not for x being bound_QC-variable holds x in still_not-bound_in f
still_not-bound_in f <> bound_QC-variables by Th63, Th64;
then not for b being set holds
( b in still_not-bound_in f iff b in bound_QC-variables ) by TARSKI:1;
then consider b being set such that
A1: not b in still_not-bound_in f and
A2: b in bound_QC-variables ;
reconsider x = b as bound_QC-variable 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