let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- ('not' p) => q & X |- 'not' q holds
X |- p
let p, q be Element of CQC-WFF A; :: thesis: for X being Subset of (CQC-WFF A) st X |- ('not' p) => q & X |- 'not' q holds
X |- p
let X be Subset of (CQC-WFF A); :: 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 Th74;
hence ( not X |- 'not' q or X |- p ) by CQC_THE1:55; :: thesis: verum