theorem :: CQC_THE1:45

for Al being QC-alphabet
for p, q being Element of CQC-WFF Al holds (p '&' q) => (q '&' p) in TAUT Al