:: deftheorem defines Quant SUBSTUT1:def 37 :
for A being QC-alphabet
for S being Element of QC-Sub-WFF A
for p being QC-formula of A holds Quant (S,p) = All ((S_Bound (@ S)),p);