let p, q be Element of CQC-WFF ; :: thesis: ( p '&' q in TAUT implies p 'or' q in TAUT )
assume A1: p '&' q in TAUT ; :: thesis: p 'or' q in TAUT
(p '&' q) => (p 'or' q) in TAUT by Th20;
hence p 'or' q in TAUT by A1, CQC_THE1:82; :: thesis: verum