:: deftheorem defines quantifiable SUBSTUT1:def 22 :
for A being QC-alphabet
for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] holds
( B is quantifiable iff ex e being Element of vSUB A st (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),e] );