let Al be QC-alphabet ; :: thesis: for S being Element of CQC-Sub-WFF Al st S is Sub_universal holds
CQC_Sub S = CQCQuant (S,(CQC_Sub (CQCSub_the_scope_of S)))
let S be Element of CQC-Sub-WFF Al; :: thesis: ( S is Sub_universal implies CQC_Sub S = CQCQuant (S,(CQC_Sub (CQCSub_the_scope_of S))) )
assume A1: S is Sub_universal ; :: thesis: CQC_Sub S = CQCQuant (S,(CQC_Sub (CQCSub_the_scope_of S)))
then CQCSub_the_scope_of S = Sub_the_scope_of S by Def6;
then CQCQuant (S,(CQC_Sub (CQCSub_the_scope_of S))) = Quant (S,(CQC_Sub (Sub_the_scope_of S))) by A1, Def7;
hence CQC_Sub S = CQCQuant (S,(CQC_Sub (CQCSub_the_scope_of S))) by A1, SUBSTUT1:32; :: thesis: verum