:: deftheorem defines Dom_Bound_Vars SUBSTUT1:def 9 :
for A being QC-alphabet
for p being QC-formula of A holds Dom_Bound_Vars p = { s where s is QC-symbol of A : x. s in Bound_Vars p } ;