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 that
A2: not k = 1 and
A3: not k = 2 ; :: thesis: contradiction
A4: ( k < 2 or k > 2 ) by A3, XXREAL_0:1;
( k = 0 or k > 1 ) by A2, NAT_2:19;
hence contradiction by A1, A4, Th21, Th46, PRE_FF:1; :: thesis: verum

end;

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