let X, Y be Subset of CQC-WFF ; :: 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