let p, q be Element of CQC-WFF ; :: thesis: ( p '&' q is valid implies ( p is valid & q is valid ) )
assume A1: p '&' q is valid ; :: thesis: ( p is valid & q is valid )
( (p '&' q) => p is valid & (p '&' q) => q is valid ) by Lm1;
hence ( p is valid & q is valid ) by A1, CQC_THE1:65; :: thesis: verum