:: deftheorem defines RestrictSub SUBSTUT1:def 6 :
for A being QC-alphabet
for x being bound_QC-variable of A
for p being QC-formula of A
for Sub being CQC_Substitution of A holds RestrictSub (x,p,Sub) = Sub | { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ;