let T be Subset of MC-wff; :: thesis: ( T is S4_theory iff CnS4 T = T )

hereby :: thesis: ( CnS4 T = T implies T is S4_theory )

assume A1: T is S4_theory ; :: thesis: CnS4 T = T
A2: CnS4 T c= T

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in CnS4 T or a in T )
assume a in CnS4 T ; :: thesis: a in T
hence a in T by A1, Def23; :: thesis: verum

end;

T c= CnS4 T by Th89;
hence CnS4 T = T by A2, XBOOLE_0:def 10; :: thesis: verum

end;

thus ( CnS4 T = T implies T is S4_theory ) ; :: thesis: verum