assume not Seg n is empty ; :: thesis: contradiction
then consider x being set such that
A1: x in Seg n by XBOOLE_0:def 1;
ex k being Element of NAT st
( k = x & 1 <= k & k <= 0 ) by A1;
hence contradiction ; :: thesis: verum