let n be Nat; :: thesis: ( n > 4 implies ex k being Nat st
( ( n = 2 * k & k > 2 ) or ( n = (2 * k) + 1 & k > 1 ) ) )
assume A1: n > 4 ; :: thesis: ex k being Nat st
( ( n = 2 * k & k > 2 ) or ( n = (2 * k) + 1 & k > 1 ) )

per cases ( n is even or n is odd ) ;

suppose n is even ; :: thesis: ex k being Nat st
( ( n = 2 * k & k > 2 ) or ( n = (2 * k) + 1 & k > 1 ) )

then consider k being Nat such that
A2: n = 2 * k ;
take k ; :: thesis: ( ( n = 2 * k & k > 2 ) or ( n = (2 * k) + 1 & k > 1 ) )
4 = 2 * 2 ;
hence ( ( n = 2 * k & k > 2 ) or ( n = (2 * k) + 1 & k > 1 ) ) by A1, A2, XREAL_1:66; :: thesis: verum

end;

suppose n is odd ; :: thesis: ex k being Nat st
( ( n = 2 * k & k > 2 ) or ( n = (2 * k) + 1 & k > 1 ) )

then consider k being Nat such that
A3: n = (2 * k) + 1 by ABIAN:9;
take k ; :: thesis: ( ( n = 2 * k & k > 2 ) or ( n = (2 * k) + 1 & k > 1 ) )

now :: thesis: not k <= 1

assume k <= 1 ; :: thesis: contradiction
then 2 * k <= 2 * 1 by XREAL_1:64;
then (2 * k) + 1 <= 2 + 1 by XREAL_1:6;
hence contradiction by A1, A3, XXREAL_0:2; :: thesis: verum

end;

hence ( ( n = 2 * k & k > 2 ) or ( n = (2 * k) + 1 & k > 1 ) ) by A3; :: thesis: verum

end;

end;