theorem Th27: :: CQC_THE3:27

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