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