let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A st p is valid & q is valid holds
p '&' q is valid
let p, q be Element of CQC-WFF A; :: thesis: ( p is valid & q is valid implies p '&' q is valid )
assume ( p in TAUT A & q in TAUT A ) ; :: according to CQC_THE1:def 10 :: thesis: p '&' q is valid
hence p '&' q in TAUT A by PROCAL_1:47; :: according to CQC_THE1:def 10 :: thesis: verum