:: deftheorem defines valid_IPC INTPRO_2:def 9 :
for s being MC-formula holds
( s is valid_IPC iff s in IPC-Taut );