let X be Subset of CQC-WFF; :: thesis: X |- TAUT
TAUT c= Cn X by CQC_THE1:75;
hence X |- TAUT by Th7; :: thesis: verum