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