theorem Th3: :: GLIB_006:3

for i, j being Nat st i > (i -' 1) + j holds
j = 0