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
CQCQuant (CQCSub_All [S,x],xSQ),(CQC_Sub S) = All (S_Bound (@ (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
CQCQuant (CQCSub_All [S,x],xSQ),(CQC_Sub S) = All (S_Bound (@ (CQCSub_All [S,x],xSQ))),(CQC_Sub S)
let xSQ be second_Q_comp of [S,x]; :: thesis: ( [S,x] is quantifiable implies CQCQuant (CQCSub_All [S,x],xSQ),(CQC_Sub S) = All (S_Bound (@ (CQCSub_All [S,x],xSQ))),(CQC_Sub S) )
set S1 = CQCSub_All [S,x],xSQ;
set p = CQC_Sub (CQCSub_the_scope_of (CQCSub_All [S,x],xSQ));
A1: Quant (CQCSub_All [S,x],xSQ),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All [S,x],xSQ))) = All (S_Bound (@ (CQCSub_All [S,x],xSQ))),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All [S,x],xSQ))) by SUBSTUT1:def 37;
assume A2: [S,x] is quantifiable ; :: thesis: CQCQuant (CQCSub_All [S,x],xSQ),(CQC_Sub S) = All (S_Bound (@ (CQCSub_All [S,x],xSQ))),(CQC_Sub S)
then CQCSub_All [S,x],xSQ = Sub_All [S,x],xSQ by Def6;
then CQCSub_All [S,x],xSQ is Sub_universal by A2, SUBSTUT1:14;
then A3: CQCQuant (CQCSub_All [S,x],xSQ),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All [S,x],xSQ))) = Quant (CQCSub_All [S,x],xSQ),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All [S,x],xSQ))) by Def8;
CQCQuant (CQCSub_All [S,x],xSQ),(CQC_Sub S) = CQCQuant (CQCSub_All [S,x],xSQ),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All [S,x],xSQ))) by A2, Th31;
hence CQCQuant (CQCSub_All [S,x],xSQ),(CQC_Sub S) = All (S_Bound (@ (CQCSub_All [S,x],xSQ))),(CQC_Sub S) by A2, A3, A1, Th31; :: thesis: verum