let A be QC-alphabet ; for c being Element of fixed_QC-variables A
for a being Element of free_QC-variables A holds c <> a
let c be Element of fixed_QC-variables A; for a being Element of free_QC-variables A holds c <> a
let a be Element of free_QC-variables A; c <> a
consider a1, a2 being object such that
A1:
a1 in {6}
and
a2 in NAT
and
A2:
a = [a1,a2]
by ZFMISC_1:def 2;
consider c1, c2 being object such that
A3:
c1 in {5}
and
c2 in QC-symbols A
and
A4:
c = [c1,c2]
by ZFMISC_1:def 2;
A5:
c1 = 5
by A3, TARSKI:def 1;
a1 = 6
by A1, TARSKI:def 1;
hence
c <> a
by A2, A4, A5, XTUPLE_0:1; verum