let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A holds
( ('not' p) => ('not' q) is valid iff q => p is valid )
let p, q be Element of CQC-WFF A; :: thesis: ( ('not' p) => ('not' q) is valid iff q => p is valid )
thus ( ('not' p) => ('not' q) is valid implies q => p is valid ) :: thesis: ( q => p is valid implies ('not' p) => ('not' q) is valid )

proof

assume A1: ('not' p) => ('not' q) is valid ; :: thesis: q => p is valid
(('not' p) => ('not' q)) => (q => p) is valid ;
hence q => p is valid by A1, CQC_THE1:65; :: thesis: verum

end;

assume A2: q => p is valid ; :: thesis: ('not' p) => ('not' q) is valid
(q => p) => (('not' p) => ('not' q)) is valid ;
hence ('not' p) => ('not' q) is valid by A2, CQC_THE1:65; :: thesis: verum