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