let n be Nat; :: thesis: Fib (n + 3) = (Fib (n + 2)) + (Fib (n + 1))
Fib (n + 3) = Fib ((n + 1) + 2)
.= (Fib ((n + 1) + 1)) + (Fib (n + 1)) by Th24
.= (Fib (n + 2)) + (Fib (n + 1)) ;
hence Fib (n + 3) = (Fib (n + 2)) + (Fib (n + 1)) ; :: thesis: verum