:: deftheorem defines Sub_the_bound_of SUBSTUT1:def 33 :
for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_universal holds
for b₃ being bound_QC-variable of A holds
( b₃ = Sub_the_bound_of S iff ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( S = Sub_All (B,SQ) & B `2 = b₃ & B is quantifiable ) );