theorem Th10: :: NUMBER16:10

for j being Nat st 0 < j & j <= 7 holds
ex i being Nat st
( i > 0 & Fib 0, Fib i are_congruent_mod j & Fib 1, Fib (i + 1) are_congruent_mod j )