let A be QC-alphabet ; :: thesis: for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]
for SQ being second_Q_comp of B st B is quantifiable holds
Sub_the_scope_of (Sub_All (B,SQ)) = B `1
let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]; :: 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 ;
hence Sub_the_scope_of (Sub_All (B,SQ)) = B `1 by A1, Def34; :: thesis: verum