let p, q be Element of CQC-WFF ; :: thesis: ( p is valid & q is valid implies p '&' q is valid )
assume ( p in TAUT & q in TAUT ) ; :: according to CQC_THE1:def 11 :: thesis: p '&' q is valid
hence p '&' q in TAUT by PROCAL_1:47; :: according to CQC_THE1:def 11 :: thesis: verum