let p be Element of CQC-WFF ; :: thesis: ( ( for Sub being CQC_Substitution holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) implies for Sub being CQC_Substitution holds QuantNbr ('not' p) = QuantNbr (CQC_Sub [('not' p),Sub]) )
assume A1: for Sub being CQC_Substitution holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ; :: thesis: for Sub being CQC_Substitution holds QuantNbr ('not' p) = QuantNbr (CQC_Sub [('not' p),Sub])
let Sub be CQC_Substitution; :: thesis: QuantNbr ('not' p) = QuantNbr (CQC_Sub [('not' p),Sub])
set S = [('not' p),Sub];
[('not' p),Sub] = Sub_not [p,Sub] by Th16;
then QuantNbr (CQC_Sub [('not' p),Sub]) = QuantNbr ('not' (CQC_Sub [p,Sub])) by SUBSTUT1:29
.= QuantNbr (CQC_Sub [p,Sub]) by CQC_SIM1:16
.= QuantNbr p by A1 ;
hence QuantNbr ('not' p) = QuantNbr (CQC_Sub [('not' p),Sub]) by CQC_SIM1:16; :: thesis: verum