let Al be QC-alphabet ; :: thesis: 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; :: thesis: for Sub being CQC_Substitution of Al holds [('not' p),Sub] = Sub_not [p,Sub]
let Sub be CQC_Substitution of Al; :: thesis: [('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] ; :: thesis: verum