theorem Th17: :: INTPRO_1:17

for p being Element of MC-wff holds p => p in IPC-Taut