n in omega by ORDINAL1:def 13;
hence Segm n is Subset of omega by ORDINAL1:26; :: thesis: verum