let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A ex t being QC-symbol of A st x. t = x
let x be bound_QC-variable of A; :: thesis: ex t being QC-symbol of A st x. t = x
consider i, t being object such that
A1: i in {4} and
A2: t in QC-symbols A and
A3: [i,t] = x by ZFMISC_1:def 2;
reconsider t = t as QC-symbol of A by A2;
take t ; :: thesis: x. t = x
thus x. t = x by A1, A3, TARSKI:def 1; :: thesis: verum