let X be Subset of MC-wff; :: thesis: for p being Element of MC-wff holds X |-_IPC p => p
let p be Element of MC-wff ; :: thesis: X |-_IPC p => p
A1: X |-_IPC p => (p => p) by INTPRO_1:1;
A2: X |-_IPC p => ((p => p) => p) by INTPRO_1:1;
X |-_IPC (p => ((p => p) => p)) => ((p => (p => p)) => (p => p)) by INTPRO_1:2;
then X |-_IPC (p => (p => p)) => (p => p) by A2, Th27;
hence X |-_IPC p => p by A1, Th27; :: thesis: verum