n in omega by ORDINAL1:def 12;
hence Segm n is Subset of omega by ORDINAL1:16; :: thesis: verum