let p, q be Element of CQC-WFF ; :: thesis: ( p in TAUT & q in TAUT implies p '&' q in TAUT )
assume that
A1: p in TAUT and
A2: q in TAUT ; :: thesis: p '&' q in TAUT
p => (q => (p '&' q)) in TAUT by Th28;
then q => (p '&' q) in TAUT by A1, CQC_THE1:46;
hence p '&' q in TAUT by A2, CQC_THE1:46; :: thesis: verum