let X, Y, Z be Subset of CQC-WFF; :: thesis: ( X |- Y & Y |- Z implies X |- Z )
assume that
A1: X |- Y and
A2: Y |- Z ; :: thesis: X |- Z
for p being Element of CQC-WFF st p in Z holds
X |- p

proof

let p be Element of CQC-WFF ; :: thesis: ( p in Z implies X |- p )
assume p in Z ; :: thesis: X |- p
then Y |- p by A2, Def2;
then A3: p in Cn Y by CQC_THE1:def 9;
Y c= Cn X by A1, Th7;
then Cn Y c= Cn X by CQC_THE1:36, CQC_THE1:37;
hence X |- p by A3, CQC_THE1:def 9; :: thesis: verum

end;

hence X |- Z by Def2; :: thesis: verum