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;
A3: 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 A4: a in Cn T ; :: thesis: a in T
thus a in T by A1, A4, Def2; :: thesis: verum

end;

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

end;

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