assume not Seg n is empty ; :: thesis: contradiction
then consider x being object such that
A1: x in Seg n ;
ex k being Nat st
( k = x & 1 <= k & k <= 0 ) by A1;
hence contradiction ; :: thesis: verum