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