theorem Th54: :: INTPRO_1:54

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