let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A st p => ('not' q) is valid holds
q => ('not' p) is valid
let p, q be Element of CQC-WFF A; :: thesis: ( p => ('not' q) is valid implies q => ('not' p) is valid )
assume A1: p => ('not' q) is valid ; :: thesis: q => ('not' p) is valid
(p => ('not' q)) => (q => ('not' p)) is valid ;
hence q => ('not' p) is valid by A1, CQC_THE1:65; :: thesis: verum