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