let Al be QC-alphabet ; :: thesis: for T being Subset of (CQC-WFF Al) st T is being_a_theory holds
TAUT Al c= T
let T be Subset of (CQC-WFF Al); :: thesis: ( T is being_a_theory implies TAUT Al c= T )
assume A1: T is being_a_theory ; :: thesis: TAUT Al c= T
Cn ({} (CQC-WFF Al)) c= Cn T by Th14, XBOOLE_1:2;
hence TAUT Al c= T by A1, Th16; :: thesis: verum