theorem :: INTPRO_2:32

for p, q being Element of MC-wff holds |-_IPC p => (p 'or' q) by Th23;