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