theorem Th92: :: INTPRO_1:92

for T being Subset of MC-wff holds
( T is S4_theory iff CnS4 T = T )