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