let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A holds
( (p '&' q) => p is valid & (p '&' q) => q is valid )
let p, q be Element of CQC-WFF A; :: thesis: ( (p '&' q) => p is valid & (p '&' q) => q is valid )
thus ( (p '&' q) => p in TAUT A & (p '&' q) => q in TAUT A ) by PROCAL_1:19, PROCAL_1:21; :: according to CQC_THE1:def 10 :: thesis: verum