let x be bound_QC-variable; :: thesis: for S being Element of CQC-Sub-WFF
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 ; :: thesis: 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]; :: thesis: ( [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 ; :: thesis: ( 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 Th30;
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) ) by MCART_1:7; :: thesis: verum