let p, q be Element of CQC-WFF ; :: thesis: (p 'or' q) <=> (q 'or' p) in TAUT
set P = p 'or' q;
set Q = q 'or' p;
( (p 'or' q) => (q 'or' p) in TAUT & (q 'or' p) => (p 'or' q) in TAUT ) by Th8;
then ((p 'or' q) => (q 'or' p)) '&' ((q 'or' p) => (p 'or' q)) in TAUT by Lm4;
hence (p 'or' q) <=> (q 'or' p) in TAUT by QC_LANG2:def 4; :: thesis: verum