let t, u, v be GRZ-formula; :: thesis: ( t => u is LD-provable & u => v is LD-provable implies t => v is LD-provable )
assume A1: ( t => u is LD-provable & u => v is LD-provable ) ; :: thesis: t => v is LD-provable
set x = LD-EqClassOf t;
set y = LD-EqClassOf u;
set z = LD-EqClassOf v;
A2: ( LD-EqClassOf (t => u) = (LD-EqClassOf t) => (LD-EqClassOf u) & LD-EqClassOf (u => v) = (LD-EqClassOf u) => (LD-EqClassOf v) ) by Th97;
LD-EqClassOf (t => v) = (LD-EqClassOf t) => (LD-EqClassOf v) by Th97;
hence t => v is LD-provable by A1, A2, Th90, Th101; :: thesis: verum