let n be Element of NAT ; :: thesis: ( n > 1 & n <> 4 & Fib n is prime implies n is prime )
assume that
A1: n > 1 and
A2: n <> 4 ; :: thesis: ( not Fib n is prime or n is prime )
assume A3: Fib n is prime ; :: thesis: n is prime
assume not n is prime ; :: thesis: contradiction
then consider k being non zero Element of NAT such that
A4: k <> 1 and
A5: k <> 2 and
A6: k <> n and
A7: k divides n by A1, A2, Th49;
A8: Fib k <> Fib n by A1, A4, A6, Th48;
( Fib k <> 1 & Fib k divides Fib n ) by A4, A5, A7, Th42, Th47;
hence contradiction by A3, A8, INT_2:def 4; :: thesis: verum