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