let A be QC-alphabet ; :: thesis: for p, q, r being Element of CQC-WFF A st p |-| q & q |-| r holds
p |-| r
let p, q, r be Element of CQC-WFF A; :: thesis: ( p |-| q & q |-| r implies p |-| r )
assume that
A1: p |-| q and
A2: q |-| r ; :: thesis: p |-| r
A3: r |- q by A2, Def5;
q |- p by A1, Def5;
then A4: r |- p by A3, Th6;
A5: q |- r by A2, Def5;
p |- q by A1, Def5;
then p |- r by A5, Th6;
hence p |-| r by A4, Def5; :: thesis: verum