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 `1 ; :: 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 `1 = B `1 & 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 `1 = B `1 & B is quantifiable ) by A2; :: thesis: verum