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