:: deftheorem Def6 defines |-_IPC INTPRO_2:def 6 :
for X being Subset of MC-wff
for s being MC-formula holds
( X |-_IPC s iff s in CnIPC X );