let X be Subset of CQC-WFF; :: thesis: X |-| Cn X
Cn X = Cn (Cn X) by CQC_THE1:19;
hence X |-| Cn X by Th20; :: thesis: verum