let x, y, z be LD-EqClass; :: thesis: ( x => y is LD-provable & y => z is LD-provable implies x => z is LD-provable )
assume that
A1: x => y is LD-provable and
A2: y => z is LD-provable ; :: thesis: x => z is LD-provable
x = x '&' y by A1, Th92
.= x '&' (y '&' z) by A2, Th92
.= (x '&' y) '&' z by Th98
.= x '&' z by A1, Th92 ;
hence x => z is LD-provable by Th92; :: thesis: verum