for Al being QC-alphabet
for T, X being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds
Cn X c= T by Def2;