let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al) holds Cn (Cn X) = Cn X
let X be Subset of (CQC-WFF Al); :: thesis: Cn (Cn X) = Cn X
( Cn (Cn X) c= Cn X & Cn X c= Cn (Cn X) ) by Lm1, Th17;
hence Cn (Cn X) = Cn X by XBOOLE_0:def 10; :: thesis: verum