1 <= n by NAT_1:14;
then 1 in Seg n ;
hence not Seg n is empty ; :: thesis: verum