theorem :: INTPRO_2:33

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