theorem Th26: :: CQC_THE3:26

for A being QC-alphabet
for Y, Z, X1, X2 being Subset of (CQC-WFF A) st X1 |-| X2 & X1 \/ Y |- Z holds
X2 \/ Y |- Z