let X be Subset of MC-wff; :: thesis: for p being Element of MC-wff st p in X holds
p in CnIPC X
let p be Element of MC-wff ; :: thesis: ( p in X implies p in CnIPC X )
assume p in X ; :: thesis: p in CnIPC X
then X |-_IPC p by Th67;
hence p in CnIPC X ; :: thesis: verum