let A be QC-alphabet ; for x being bound_QC-variable of A holds not x in fixed_QC-variables A
let x be bound_QC-variable of A; not x in fixed_QC-variables A
x in bound_QC-variables A
;
then
x in [:{4},(QC-symbols A):]
by QC_LANG1:def 4;
then consider x1, x2 being object such that
A1:
x1 in {4}
and
x2 in QC-symbols A
and
A2:
x = [x1,x2]
by ZFMISC_1:def 2;
A3:
x1 = 4
by A1, TARSKI:def 1;
assume
x in fixed_QC-variables A
; contradiction
then
x in [:{5},(QC-symbols A):]
by QC_LANG1:def 5;
then consider c1, c2 being object such that
A4:
c1 in {5}
and
c2 in QC-symbols A
and
A5:
x = [c1,c2]
by ZFMISC_1:def 2;
c1 = 5
by A4, TARSKI:def 1;
hence
contradiction
by A2, A5, A3, XTUPLE_0:1; verum