let A be QC-alphabet ; :: thesis: for Y, X1, X2 being Subset of (CQC-WFF A) st X1 |-| X2 holds
X1 \/ Y |-| X2 \/ Y
let Y, X1, X2 be Subset of (CQC-WFF A); :: 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