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));
assume A1: [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 A2: CQCSub_All [S,x],xSQ is Sub_universal by A1, SUBSTUT1:14;
A3: 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 A1, Th31;
A4: 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 A2, Def8;
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;
hence CQCQuant (CQCSub_All [S,x],xSQ),(CQC_Sub S) = All (S_Bound (@ (CQCSub_All [S,x],xSQ))),(CQC_Sub S) by A1, A3, A4, Th31; :: thesis: verum