let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A st p '&' q is valid holds
( p is valid & q is valid )
let p, q be Element of CQC-WFF A; :: 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