let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A holds (p '&' ('not' p)) => q in TAUT A
let p, q be Element of CQC-WFF A; :: thesis: (p '&' ('not' p)) => q in TAUT A
('not' q) => ('not' (p '&' ('not' p))) in TAUT A by Th1, LUKASI_1:13;
hence (p '&' ('not' p)) => q in TAUT A by LUKASI_1:35; :: thesis: verum