let B be Element of [:QC-Sub-WFF ,bound_QC-variables :]; :: thesis: for SQ being second_Q_comp of B st B is quantifiable holds
( (Sub_All B,SQ) `1 = All (B `2 ),((B `1 ) `1 ) & (Sub_All B,SQ) `2 = SQ )
let SQ be second_Q_comp of B; :: thesis: ( B is quantifiable implies ( (Sub_All B,SQ) `1 = All (B `2 ),((B `1 ) `1 ) & (Sub_All B,SQ) `2 = SQ ) )
assume B is quantifiable ; :: thesis: ( (Sub_All B,SQ) `1 = All (B `2 ),((B `1 ) `1 ) & (Sub_All B,SQ) `2 = SQ )
then Sub_All B,SQ = [(All (B `2 ),((B `1 ) `1 )),SQ] by SUBSTUT1:def 24;
hence ( (Sub_All B,SQ) `1 = All (B `2 ),((B `1 ) `1 ) & (Sub_All B,SQ) `2 = SQ ) by MCART_1:7; :: thesis: verum