let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A holds p '&' q |-| q '&' p
let p, q be Element of CQC-WFF A; :: thesis: p '&' q |-| q '&' p
A1: {q,p} |-| {(q '&' p)} by Th31;
{(p '&' q)} |-| {q,p} by Th31;
then {(p '&' q)} |-| {(q '&' p)} by A1;
hence p '&' q |-| q '&' p by Th29; :: thesis: verum