for Al being QC-alphabet
for T being Subset of (CQC-WFF Al) st T is being_a_theory holds
TAUT Al c= T