let k be Nat; :: thesis: ( Fib k = 1 iff ( k = 1 or k = 2 ) )
( not Fib k = 1 or k = 1 or k = 2 )

proof

assume A1: Fib k = 1 ; :: thesis: ( k = 1 or k = 2 )
assume ( not k = 1 & not k = 2 ) ; :: thesis: contradiction
then ( ( k = 0 or k > 1 ) & ( k < 2 or k > 2 ) ) by NAT_2:21, XXREAL_0:1;
hence contradiction by A1, Th23, Th48, PRE_FF:1; :: thesis: verum

end;

hence ( Fib k = 1 iff ( k = 1 or k = 2 ) ) by Th23, PRE_FF:1; :: thesis: verum