let X1, X2, Y be Subset of CQC-WFF; :: 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