theorem :: NUMBER06:48

for k, l, m, n being Nat holds
( not 0 < k or not k < l or not l < m or not m < n or not (Fib m) - (Fib l) = (Fib l) - (Fib k) or not (Fib l) - (Fib k) = (Fib n) - (Fib m) or not (Fib l) - (Fib k) > 0 )