:: deftheorem Def24 defines Sub_All SUBSTUT1:def 24 :
for A being QC-alphabet
for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]
for SQ being second_Q_comp of B st B is quantifiable holds
Sub_All (B,SQ) = [(All ((B `2),((B `1) `1))),SQ];