let p, q be Element of CQC-WFF ; :: thesis: for X being Subset of CQC-WFF st X |- p => ('not' q) & X |- q holds
X |- 'not' p
let X be Subset of CQC-WFF ; :: thesis: ( X |- p => ('not' q) & X |- q implies X |- 'not' p )
assume X |- p => ('not' q) ; :: thesis: ( not X |- q or X |- 'not' p )
then X |- q => ('not' p) by Th90;
hence ( not X |- q or X |- 'not' p ) by CQC_THE1:92; :: thesis: verum