:: deftheorem Def28 defines Sub_universal SUBSTUT1:def 28 :
for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( S is Sub_universal 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 is quantifiable ) );