let p, q be Element of CQC-WFF ; :: 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:25;
then ('not' p) => ('not' q) is valid by A2, Th41;
then q => p is valid by LUKASI_1:63;
hence q |- p by Th39; :: thesis: verum