let T be Subset of CQC-WFF; :: thesis: ( T is being_a_theory iff Cn T = T )
thus ( T is being_a_theory implies Cn T = T ) :: thesis: ( Cn T = T implies T is being_a_theory )

proof

assume A1: T is being_a_theory ; :: thesis: Cn T = T
A2: T c= Cn T by Th38;
Cn T c= T

proof

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

end;

hence Cn T = T by A2, XBOOLE_0:def 10; :: thesis: verum

end;

thus ( Cn T = T implies T is being_a_theory ) by Th36; :: thesis: verum