:: deftheorem defines upVar SUBSTUT1:def 12 :
for A being QC-alphabet
for finSub being finite CQC_Substitution of A
for p being QC-formula of A holds upVar (finSub,p) = the Element of NSub (p,finSub);