theorem Th56: :: INTPRO_1:56

for p, q being Element of MC-wff holds (p 'or' q) => (q 'or' p) in IPC-Taut