for Al being QC-alphabet
for X being Subset of (CQC-WFF Al) holds Cn X is being_a_theory by Th2, Th3, Th4, Th5, Th6, Th7, Th8, Th9, Th10;