theorem :: QC_LANG3:30

for A being QC-alphabet
for x being bound_QC-variable of A ex t being QC-symbol of A st x. t = x