take 1 ; :: thesis: 1 is Fibonacci
thus 1 is Fibonacci by PRE_FF:1; :: thesis: verum