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 is Sub_universal
let SQ be second_Q_comp of B; :: thesis: ( B is quantifiable implies Sub_All B,SQ is Sub_universal )
assume A1: B is quantifiable ; :: thesis: Sub_All B,SQ is Sub_universal
take B ; :: according to SUBSTUT1:def 28 :: thesis: ex SQ being second_Q_comp of B st
( Sub_All B,SQ = Sub_All B,SQ & B is quantifiable )
take SQ ; :: thesis: ( Sub_All B,SQ = Sub_All B,SQ & B is quantifiable )
thus ( Sub_All B,SQ = Sub_All B,SQ & B is quantifiable ) by A1; :: thesis: verum