:: deftheorem Def2 defines Cn CQC_THE1:def 2 :
for Al being QC-alphabet
for X, b₃ being Subset of (CQC-WFF Al) holds
( b₃ = Cn X iff for t being Element of CQC-WFF Al holds
( t in b₃ iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds
t in T ) );