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