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
for p being Element of CQC-WFF A st p in Z holds
X |- p
proof
let p be Element of CQC-WFF A; :: thesis: ( p in Z implies X |- p )
assume p in Z ; :: thesis: X |- p
then Y |- p by A2;
then A3: p in Cn Y by CQC_THE1:def 8;
Y c= Cn X by A1, Th7;
then Cn Y c= Cn X by CQC_THE1:15, CQC_THE1:16;
hence X |- p by A3, CQC_THE1:def 8; :: thesis: verum
end;
hence X |- Z ; :: thesis: verum