:: deftheorem Def34 defines Sub_the_scope_of SUBSTUT1:def 34 :
for A being QC-alphabet
for A2 being Element of QC-Sub-WFF A st A2 is Sub_universal holds
for b₃ being Element of QC-Sub-WFF A holds
( b₃ = Sub_the_scope_of A2 iff ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st
( A2 = Sub_All (B,SQ) & B `1 = b₃ & B is quantifiable ) );