theorem :: INTPRO_1:95

IPC-Taut c= S4-Taut by Th81;