let q, r be Element of MC-wff ; :: thesis: {q} |-_IPC q 'or' r
A1: {q} |-_IPC q by Th65;
{q} |-_IPC q => (q 'or' r) by Th23;
hence {q} |-_IPC q 'or' r by A1, Th27; :: thesis: verum