let n be Element of NAT ; :: thesis: ( n > 1 & n <> 4 & Fib n is prime implies n is prime )
assume A1: ( n > 1 & n <> 4 ) ; :: thesis: ( not Fib n is prime or n is prime )
assume A2: Fib n is prime ; :: thesis: n is prime
assume not n is prime ; :: thesis: contradiction
then consider k being non empty Element of NAT such that
A3: ( k <> 1 & k <> 2 & k <> n & k divides n ) by A1, Th51;
A4: Fib k <> 1 by A3, Th49;
A5: Fib k <> Fib n by A1, A3, Th50;
Fib k divides Fib n by A3, Th44;
hence contradiction by A2, A4, A5, INT_2:def 5; :: thesis: verum