let n be Nat; :: thesis: ( Fib n > 1 implies n > 2 )
assume A1: Fib n > 1 ; :: thesis: n > 2
assume n <= 2 ; :: thesis: contradiction
then ( n = 2 or n < 2 ) by XXREAL_0:1;
hence contradiction by A1, FIB_NUM2:47, PRE_FF:1, NAT_1:23; :: thesis: verum