theorem Th101: :: GRZLOG_1:44

for x, y, z being LD-EqClass st x => y is LD-provable & y => z is LD-provable holds
x => z is LD-provable