let n be non zero even Nat; :: thesis: 1 in Segm n
consider k being Nat such that
A1: n = 2 * k by ABIAN:def 2;
k <> 0 by A1;
then 1 <= k by NAT_1:25;
then A2: 2 * 1 <= 2 * k by XREAL_1:64;
( n > 1 or n = 0 or n = 1 ) by NAT_1:25;
hence 1 in Segm n by A1, A2, NAT_1:44; :: thesis: verum