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