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