let p, q be Element of MC-wff ; :: thesis: (p 'or' q) => (q 'or' p) in IPC-Taut
A1: (p => (q 'or' p)) => ((q => (q 'or' p)) => ((p 'or' q) => (q 'or' p))) in IPC-Taut by Def14;
A2: p => (q 'or' p) in IPC-Taut by Def14;
A3: q => (q 'or' p) in IPC-Taut by Def14;
(q => (q 'or' p)) => ((p 'or' q) => (q 'or' p)) in IPC-Taut by A1, A2, Def14;
hence (p 'or' q) => (q 'or' p) in IPC-Taut by A3, Def14; :: thesis: verum