let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A st p is closed & p |- q holds
'not' q |- 'not' p
let p, q be Element of CQC-WFF A; :: thesis: ( p is closed & p |- q implies 'not' q |- 'not' p )
assume that
A1: p is closed and
A2: p |- q ; :: thesis: 'not' q |- 'not' p
p => q is valid by A1, A2, Th41;
then ('not' q) => ('not' p) is valid by LUKASI_1:52;
hence 'not' q |- 'not' p by Th39; :: thesis: verum