let p, q be Element of CQC-WFF ; :: 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:63;
hence 'not' q |- 'not' p by Th39; :: thesis: verum