let X, Y be Subset of CQC-WFF; :: thesis: (Cn X) \/ (Cn Y) c= Cn (X \/ Y)
A1: Cn Y c= Cn (X \/ Y) by CQC_THE1:39, XBOOLE_1:7;
Cn X c= Cn (X \/ Y) by CQC_THE1:39, XBOOLE_1:7;
hence (Cn X) \/ (Cn Y) c= Cn (X \/ Y) by A1, XBOOLE_1:8; :: thesis: verum