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