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 )
proof
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;
thus ( Cn T = T implies T is being_a_theory ) by Th11; :: thesis: verum