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