let Al be QC-alphabet ; :: thesis: ex s being set st
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds not [s,[x,p]] in QC-symbols Al
assume A1: for s being set ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st [s,[x,p]] in QC-symbols Al ; :: thesis: contradiction
for s being set holds s in union (union (QC-symbols Al))

proof

let s be set ; :: thesis: s in union (union (QC-symbols Al))
consider p being Element of CQC-WFF Al, x being bound_QC-variable of Al such that
A2: [s,[x,p]] in QC-symbols Al by A1;
A3: {s} in {{s,[x,p]},{s}} by TARSKI:def 2;
A4: s in {s} by TARSKI:def 1;
{{s,[x,p]},{s}} c= union (QC-symbols Al) by A2, ZFMISC_1:74;
then {s} c= union (union (QC-symbols Al)) by A3, ZFMISC_1:74;
hence s in union (union (QC-symbols Al)) by A4; :: thesis: verum

end;

then ( union (union (QC-symbols Al)) in union (union (QC-symbols Al)) & ( for X being set holds not X in X ) ) ;
hence contradiction ; :: thesis: verum