let p, q be Element of CQC-WFF ; :: thesis: p '&' q |-| q '&' p
A1: {(p '&' q)} |-| {q,p} by Th31;
{q,p} |-| {(q '&' p)} by Th31;
then {(p '&' q)} |-| {(q '&' p)} by A1, Th19;
hence p '&' q |-| q '&' p by Th29; :: thesis: verum