:: deftheorem defines |-_IPC INTPRO_2:def 7 :
for s being MC-formula holds
( |-_IPC s iff {} MC-wff |-_IPC s );