let A be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF A) holds X |- TAUT A
let X be Subset of (CQC-WFF A); :: thesis: X |- TAUT A
TAUT A c= Cn X by CQC_THE1:39;
hence X |- TAUT A by Th7; :: thesis: verum