let p, q be Element of CQC-WFF ; :: thesis: (('not' p) => q) => (p 'or' q) is valid
A1: (('not' p) => q) => (('not' ('not' p)) 'or' q) in TAUT by PROCAL_1:14;
('not' ('not' p)) => p in TAUT by LUKASI_1:25;
then (('not' ('not' p)) 'or' q) => (p 'or' q) in TAUT by PROCAL_1:48;
hence (('not' p) => q) => (p 'or' q) in TAUT by A1, LUKASI_1:3; :: according to CQC_THE1:def 11 :: thesis: verum