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