let p, q be Element of CQC-WFF ; :: thesis: ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) in TAUT
( ('not' ('not' p)) => p in TAUT & (('not' ('not' p)) => p) => ((p => ('not' q)) => (('not' ('not' p)) => ('not' q))) in TAUT ) by LUKASI_1:1, LUKASI_1:25;
then A1: (p => ('not' q)) => (('not' ('not' p)) => ('not' q)) in TAUT by CQC_THE1:82;
('not' (p => ('not' q))) => (p '&' q) in TAUT by Th16;
then A2: ('not' (p '&' q)) => ('not' ('not' (p => ('not' q)))) in TAUT by LUKASI_1:34;
('not' ('not' (p => ('not' q)))) => (p => ('not' q)) in TAUT by LUKASI_1:25;
then ('not' (p '&' q)) => (p => ('not' q)) in TAUT by A2, LUKASI_1:3;
then ('not' (p '&' q)) => (('not' ('not' p)) => ('not' q)) in TAUT by A1, LUKASI_1:3;
hence ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) in TAUT by Lm1; :: thesis: verum