let A be QC-alphabet ; :: thesis: for Y, X1, X2 being Subset of (CQC-WFF A) st X1 |-| X2 & Y |- X1 holds
Y |- X2
let Y, X1, X2 be Subset of (CQC-WFF A); :: thesis: ( X1 |-| X2 & Y |- X1 implies Y |- X2 )
assume that
A1: X1 |-| X2 and
A2: Y |- X1 ; :: thesis: Y |- X2
X1 |- X2 by A1, Th18;
hence Y |- X2 by A2, Th9; :: thesis: verum