let x be bound_QC-variable; :: thesis: not x in fixed_QC-variables
consider x1, x2 being set such that
A1: x1 in {4} and
x2 in NAT and
A2: x = [x1,x2] by QC_LANG1:def 2, ZFMISC_1:def 2;
A3: x1 = 4 by A1, TARSKI:def 1;
assume x in fixed_QC-variables ; :: thesis: contradiction
then consider c1, c2 being set such that
A4: c1 in {5} and
c2 in NAT and
A5: x = [c1,c2] by QC_LANG1:def 3, ZFMISC_1:def 2;
c1 = 5 by A4, TARSKI:def 1;
hence contradiction by A2, A5, A3, ZFMISC_1:33; :: thesis: verum