for t, u, v being GRZ-formula st t => u is LD-provable & u => v is LD-provable holds
t => v is LD-provable