for Al being QC-alphabet holds TAUT Al is being_a_theory by Th11;