let p, q, r be Element of CQC-WFF ; :: thesis: ( p |- q & q |- r implies p |- r )
assume that
A1: p |- q and
A2: q |- r ; :: thesis: p |- r
A3: {p} |- q by A1, Def1;
{q} |- r by A2, Def1;
then {p} |- r by A3, Th3;
hence p |- r by Def1; :: thesis: verum