let c be Element of fixed_QC-variables ; :: thesis: for a being Element of free_QC-variables holds c <> a
let a be Element of free_QC-variables ; :: thesis: c <> a
consider a1, a2 being set such that
A1: ( a1 in {6} & a2 in NAT & a = [a1,a2] ) 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;
( a1 = 6 & c1 = 5 ) by A1, A2, TARSKI:def 1;
hence c <> a by A1, A2, ZFMISC_1:33; :: thesis: verum