for Al being QC-alphabet
for T, S being Subset of (CQC-WFF Al) st T is being_a_theory & S is being_a_theory holds
T /\ S is being_a_theory