let X, Y be Subset of CQC-WFF ; :: thesis: Cn (X \/ Y) = Cn ((Cn X) \/ (Cn Y))
A1: Cn (X \/ Y) c= Cn ((Cn X) \/ (Cn Y)) by Lm1, CQC_THE1:39;
Cn ((Cn X) \/ (Cn Y)) c= Cn (X \/ Y) by Th2, Th21;
hence Cn (X \/ Y) = Cn ((Cn X) \/ (Cn Y)) by A1, XBOOLE_0:def 10; :: thesis: verum