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