let Al be QC-alphabet ; :: thesis: for B being CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
for SQ being second_Q_comp of B st B is quantifiable holds
CQCSub_the_scope_of (CQCSub_All (B,SQ)) = B `1
let B be CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]; :: thesis: for SQ being second_Q_comp of B st B is quantifiable holds
CQCSub_the_scope_of (CQCSub_All (B,SQ)) = B `1
let SQ be second_Q_comp of B; :: thesis: ( B is quantifiable implies CQCSub_the_scope_of (CQCSub_All (B,SQ)) = B `1 )
assume A1: B is quantifiable ; :: thesis: CQCSub_the_scope_of (CQCSub_All (B,SQ)) = B `1
then A2: CQCSub_All (B,SQ) = Sub_All (B,SQ) by Def5;
then CQCSub_All (B,SQ) is Sub_universal by A1, SUBSTUT1:14;
then CQCSub_the_scope_of (CQCSub_All (B,SQ)) = Sub_the_scope_of (Sub_All (B,SQ)) by A2, Def6;
hence CQCSub_the_scope_of (CQCSub_All (B,SQ)) = B `1 by A1, SUBSTUT1:21; :: thesis: verum