let Sub be CQC_Substitution; :: thesis: QuantNbr VERUM = QuantNbr (CQC_Sub [VERUM ,Sub])
[VERUM ,Sub] is Sub_VERUM by SUBSTUT1:def 19;
hence QuantNbr VERUM = QuantNbr (CQC_Sub [VERUM ,Sub]) by SUBLEMMA:3; :: thesis: verum