theorem Th16: :: CQC_THE1:20

for Al being QC-alphabet
for T being Subset of (CQC-WFF Al) holds
( T is being_a_theory iff Cn T = T )