let Al be QC-alphabet ; for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
( CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ)) = S & CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ))))) = CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub S)) )
let x be bound_QC-variable of Al; for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
( CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ)) = S & CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ))))) = CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub S)) )
let S be Element of CQC-Sub-WFF Al; for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
( CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ)) = S & CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ))))) = CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub S)) )
let xSQ be second_Q_comp of [S,x]; ( [S,x] is quantifiable implies ( CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ)) = S & CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ))))) = CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub S)) ) )
assume
[S,x] is quantifiable
; ( CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ)) = S & CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ))))) = CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub S)) )
then
CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ)) = [S,x] `1
by Th29;
hence
( CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ)) = S & CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ))))) = CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub S)) )
; verum