let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) holds
for Sub being CQC_Substitution of Al holds QuantNbr ('not' p) = QuantNbr (CQC_Sub [('not' p),Sub])
let p be Element of CQC-WFF Al; :: thesis: ( ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) implies for Sub being CQC_Substitution of Al holds QuantNbr ('not' p) = QuantNbr (CQC_Sub [('not' p),Sub]) )
assume A1: for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ; :: thesis: for Sub being CQC_Substitution of Al holds QuantNbr ('not' p) = QuantNbr (CQC_Sub [('not' p),Sub])
let Sub be CQC_Substitution of Al; :: 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