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

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