consider B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ being second_Q_comp of B such that
A2: ( A2 = Sub_All (B,SQ) & B is quantifiable ) by A1;
take B `1 ; :: thesis: 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 `1 & B is quantifiable )
thus 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 `1 & B is quantifiable ) by A2; :: thesis: verum