let p, q be Element of CQC-WFF ; :: thesis: for X being Subset of CQC-WFF st p is closed & X \/ {p} |- q holds
X \/ {('not' q)} |- 'not' p
let X be Subset of CQC-WFF; :: 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