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