let p, q be Element of CQC-WFF ; :: thesis: ('not' (p 'or' q)) => ('not' p) in TAUT
A1: (p => (p 'or' q)) => (('not' (p 'or' q)) => ('not' p)) in TAUT by LUKASI_1:26;
p => (p 'or' q) in TAUT by Th3;
hence ('not' (p 'or' q)) => ('not' p) in TAUT by A1, CQC_THE1:82; :: thesis: verum