let X be Subset of MC-wff; :: thesis: for p, q being Element of MC-wff st X |-_IPC p holds
X |-_IPC q => p
let p, q be Element of MC-wff ; :: thesis: ( X |-_IPC p implies X |-_IPC q => p )
assume A1: X |-_IPC p ; :: thesis: X |-_IPC q => p
X |-_IPC p => (q => p) by INTPRO_1:1;
hence X |-_IPC q => p by A1, INTPRO_1:10; :: thesis: verum