let Al be QC-alphabet ; 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
; contradiction
for s being set holds s in union (union (QC-symbols Al))
proof
let s be
set ;
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;
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
; verum