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