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