let p be Element of CQC-WFF ; :: thesis: p 'or' ('not' p) in TAUT
('not' p) => ('not' p) in TAUT by LUKASI_1:4;
hence p 'or' ('not' p) in TAUT by Lm1; :: thesis: verum