theorem :: INTPRO_2:49

for X being Subset of MC-wff holds X |-_IPC IVERUM by Th49, INTPRO_1:def 18;