let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st p is closed & X \/ {('not' p)} |- 'not' q holds
X \/ {q} |- p
let p, q be Element of CQC-WFF A; :: thesis: for X being Subset of (CQC-WFF A) st p is closed & X \/ {('not' p)} |- 'not' q holds
X \/ {q} |- p
let X be Subset of (CQC-WFF A); :: thesis: ( p is closed & X \/ {('not' p)} |- 'not' q implies X \/ {q} |- p )
assume that
A1: p is closed and
A2: X \/ {('not' p)} |- 'not' q ; :: thesis: X \/ {q} |- p
'not' p is closed by A1, QC_LANG3:21;
then X |- ('not' p) => ('not' q) by A2, CQC_THE2:92;
then X |- q => p by LUKASI_1:69;
hence X \/ {q} |- p by Th40; :: thesis: verum