theorem :: INTPRO_1:95
IPC-Taut c= S4-Taut by Th81;