let p be Element of MC-wff ; :: thesis: {p} |-_IPC p
( p in {p} & {p} c= CnIPC {p} ) by TARSKI:def 1, INTPRO_1:12;
hence p in CnIPC {p} ; :: according to INTPRO_2:def 6 :: thesis: verum