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