let A be QC-alphabet ; :: thesis: for Y, Z, X1, X2 being Subset of (CQC-WFF A) st X1 |-| X2 & X1 \/ Y |- Z holds
X2 \/ Y |- Z
let Y, Z, X1, X2 be Subset of (CQC-WFF A); :: thesis: ( X1 |-| X2 & X1 \/ Y |- Z implies X2 \/ Y |- Z )
assume that
A1: X1 |-| X2 and
A2: X1 \/ Y |- Z ; :: thesis: X2 \/ Y |- Z
X1 \/ Y |-| X2 \/ Y by A1, Th25;
then Cn (X1 \/ Y) = Cn (X2 \/ Y) by Th20;
then Z c= Cn (X2 \/ Y) by A2, Th7;
hence X2 \/ Y |- Z by Th7; :: thesis: verum