consider B being Element of [:QC-Sub-WFF,bound_QC-variables:], SQ being second_Q_comp of B such that
A2: ( A = Sub_All (B,SQ) & B is quantifiable ) by A1, Def28;
take B `2 ; :: thesis: ex B being Element of [:QC-Sub-WFF,bound_QC-variables:] ex SQ being second_Q_comp of B st
( A = Sub_All (B,SQ) & B `2 = B `2 & B is quantifiable )
thus ex B being Element of [:QC-Sub-WFF,bound_QC-variables:] ex SQ being second_Q_comp of B st
( A = Sub_All (B,SQ) & B `2 = B `2 & B is quantifiable ) by A2; :: thesis: verum