let T be Subset of MC-wff; :: thesis: ( T is S4_theory implies S4-Taut c= T )
assume A1: T is S4_theory ; :: thesis: S4-Taut c= T
S4-Taut c= CnS4 T by Th90, XBOOLE_1:2;
hence S4-Taut c= T by A1, Th92; :: thesis: verum