let A be QC-alphabet ; :: thesis: for X, Y being Subset of (CQC-WFF A) holds X \/ Y |-| (Cn X) \/ (Cn Y)
let X, Y be Subset of (CQC-WFF A); :: thesis: X \/ Y |-| (Cn X) \/ (Cn Y)
Cn (X \/ Y) = Cn ((Cn X) \/ (Cn Y)) by Th22;
hence X \/ Y |-| (Cn X) \/ (Cn Y) by Th20; :: thesis: verum