let T be Subset of CQC-WFF ; :: thesis: ( T is being_a_theory implies TAUT c= T )
assume A1: T is being_a_theory ; :: thesis: TAUT c= T
Cn ({} CQC-WFF ) c= Cn T by Th39, XBOOLE_1:2;
hence TAUT c= T by A1, Th41; :: thesis: verum