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 c= bound_QC-variables & 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:2;
then consider b being set such that
A1: ( not b in still_not-bound_in f & b in bound_QC-variables ) ;
reconsider x = b as bound_QC-variable by A1;
take x ; :: thesis: not x in still_not-bound_in f
thus not x in still_not-bound_in f by A1; :: thesis: verum