let X be Subset of CQC-WFF; :: thesis: Cn (Cn X) = Cn X
( Cn (Cn X) c= Cn X & Cn X c= Cn (Cn X) ) by Lm1, Th38;
hence Cn (Cn X) = Cn X by XBOOLE_0:def 10; :: thesis: verum