let Al be QC-alphabet ; :: thesis: for T being Subset of (CQC-WFF Al) holds

( T is being_a_theory iff Cn T = T )

let T be Subset of (CQC-WFF Al); :: 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 )

( T is being_a_theory iff Cn T = T )

let T be Subset of (CQC-WFF Al); :: 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

thus
( Cn T = T implies T is being_a_theory )
by Th11; :: thesis: verum
assume A1:
T is being_a_theory
; :: thesis: Cn T = T

A2: T c= Cn T by Th13;

Cn T c= T by A1, Def2;

hence Cn T = T by A2; :: thesis: verum

end;A2: T c= Cn T by Th13;

Cn T c= T by A1, Def2;

hence Cn T = T by A2; :: thesis: verum