theorem :: INTPRO_1:94

CPC-Taut c= S4-Taut by Th80;