theorem Lm2: :: DIOPHAN1:26

for k being Nat
for t being 1 _greater Nat holds [.0,((k + 1) / t).[ \/ [.((k + 1) / t),((k + 2) / t).[ = [.0,((k + 2) / t).[