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