Fib 3 = Fib ((1 + 1) + 1)
.= 2 by Th21, PRE_FF:1 ;
hence Fib 3 = 2 ; :: thesis: verum