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