let Al be QC-alphabet ; for p being Element of CQC-WFF Al
for Sub being CQC_Substitution of Al holds [('not' p),Sub] = Sub_not [p,Sub]
let p be Element of CQC-WFF Al; for Sub being CQC_Substitution of Al holds [('not' p),Sub] = Sub_not [p,Sub]
let Sub be CQC_Substitution of Al; [('not' p),Sub] = Sub_not [p,Sub]
set S = [p,Sub];
Sub_not [p,Sub] = [('not' ([p,Sub] `1)),([p,Sub] `2)]
by SUBSTUT1:def 20;
hence
[('not' p),Sub] = Sub_not [p,Sub]
; verum