let A be QC-alphabet ; :: thesis: for X, Y being Subset of (CQC-WFF A) holds (Cn X) \/ (Cn Y) c= Cn (X \/ Y)
let X, Y be Subset of (CQC-WFF A); :: thesis: (Cn X) \/ (Cn Y) c= Cn (X \/ Y)
A1: Cn Y c= Cn (X \/ Y) by CQC_THE1:18, XBOOLE_1:7;
Cn X c= Cn (X \/ Y) by CQC_THE1:18, XBOOLE_1:7;
hence (Cn X) \/ (Cn Y) c= Cn (X \/ Y) by A1, XBOOLE_1:8; :: thesis: verum