theorem Th25: :: CQC_THE3:25

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