:: deftheorem Def1 defines x. CQC_SIM1:def 1 :
for A being QC-alphabet
for b being bound_QC-variable of A
for b₃ being QC-symbol of A holds
( b₃ = x. b iff x. b₃ = b );