let A be QC-alphabet ; :: thesis: for X, Y being Subset of (CQC-WFF A) holds Cn (X \/ Y) = Cn ((Cn X) \/ (Cn Y))
let X, Y be Subset of (CQC-WFF A); :: thesis: Cn (X \/ Y) = Cn ((Cn X) \/ (Cn Y))
A1: Cn (X \/ Y) c= Cn ((Cn X) \/ (Cn Y)) by Lm1, CQC_THE1:18;
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