let X1, X2, Y be Subset of CQC-WFF; :: thesis: ( X1 |-| X2 implies X1 \/ Y |-| X2 \/ Y )
assume X1 |-| X2 ; :: thesis: X1 \/ Y |-| X2 \/ Y
then Cn X1 = Cn X2 by Th20;
then Cn (X1 \/ Y) = Cn ((Cn X2) \/ (Cn Y)) by Th22
.= Cn (X2 \/ Y) by Th22 ;
hence X1 \/ Y |-| X2 \/ Y by Th20; :: thesis: verum