let p, q be Element of CQC-WFF ; :: thesis: (p '&' q) => (q '&' p) is valid
(p '&' q) => (q '&' p) in TAUT by Def1, Th76;
hence (p '&' q) => (q '&' p) is valid by Lm13; :: thesis: verum