let k, n be Nat; :: thesis: ( k <> 1 & n <> 1 & Fib k = Fib n implies k = n )
assume that
A0: ( k <> 1 & n <> 1 ) and
A1: Fib k = Fib n and
A2: k <> n ; :: thesis: contradiction

per cases ( k < n or n < k ) by A2, XXREAL_0:1;

suppose A3: k < n ; :: thesis: contradiction

per cases ( k < 1 or k > 1 ) by A0, XXREAL_0:1;

suppose k < 1 ; :: thesis: contradiction

then k = 0 by NAT_1:14;
then Fib k = 0 by PRE_FF:1;
hence contradiction by A1, A3, LemmaFib0; :: thesis: verum

end;

suppose k > 1 ; :: thesis: contradiction

hence contradiction by A1, A3, Th46; :: thesis: verum

end;

end;

end;

suppose A4: n < k ; :: thesis: contradiction

per cases ( n < 1 or n > 1 ) by A0, XXREAL_0:1;

suppose n < 1 ; :: thesis: contradiction

then n = 0 by NAT_1:14;
then Fib n = 0 by PRE_FF:1;
hence contradiction by A1, A4, LemmaFib0; :: thesis: verum

end;

suppose n > 1 ; :: thesis: contradiction

hence contradiction by A1, A4, FIB_NUM2:46; :: thesis: verum

end;

end;

end;

end;