ex k being Nat st n = 2 * k by ABIAN:def 2;
hence n / 2 is natural ; :: thesis: verum