:: deftheorem defines . SUBSTUT2:def 1 :
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x, y being bound_QC-variable of Al holds p . (x,y) = CQC_Sub [p,(Sbst (x,y))];