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_the_scope_of (Sub_All B,SQ) = B `1
let SQ be second_Q_comp of B; :: thesis: ( B is quantifiable implies Sub_the_scope_of (Sub_All B,SQ) = B `1 )
assume A1: B is quantifiable ; :: thesis: Sub_the_scope_of (Sub_All B,SQ) = B `1
then Sub_All B,SQ is Sub_universal by Th14;
then consider B1 being Element of [:QC-Sub-WFF ,bound_QC-variables :], SQ1 being second_Q_comp of B1 such that
A2: ( Sub_All B,SQ = Sub_All B1,SQ1 & B1 `1 = Sub_the_scope_of (Sub_All B,SQ) & B1 is quantifiable ) by Def34;
thus Sub_the_scope_of (Sub_All B,SQ) = B `1 by A1, A2, Th20; :: thesis: verum