let X be Subset of MC-wff; :: thesis: for p being Element of MC-wff st p is valid_IPC holds
X |-_IPC p
let p be Element of MC-wff ; :: thesis: ( p is valid_IPC implies X |-_IPC p )
assume A1: p is valid_IPC ; :: thesis: X |-_IPC p
IPC-Taut c= CnIPC X by INTPRO_1:16;
hence X |-_IPC p by A1; :: thesis: verum