let c be Element of fixed_QC-variables ; for x being Element of bound_QC-variables holds c <> x
let x be Element of bound_QC-variables ; c <> x
consider x1, x2 being set such that
A1:
x1 in {4}
and
x2 in NAT
and
A2:
x = [x1,x2]
by ZFMISC_1:def 2;
consider c1, c2 being set such that
A3:
c1 in {5}
and
c2 in NAT
and
A4:
c = [c1,c2]
by ZFMISC_1:def 2;
A5:
c1 = 5
by A3, TARSKI:def 1;
x1 = 4
by A1, TARSKI:def 1;
hence
c <> x
by A2, A4, A5, ZFMISC_1:27; verum