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