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