let S be Element of CQC-Sub-WFF ; :: 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 Def7;
then CQCQuant S,(CQC_Sub (CQCSub_the_scope_of S)) = Quant S,(CQC_Sub (Sub_the_scope_of S)) by A1, Def8;
hence CQC_Sub S = CQCQuant S,(CQC_Sub (CQCSub_the_scope_of S)) by A1, SUBSTUT1:32; :: thesis: verum