reconsider n = n as Nat by TARSKI:1;
n in omega by ORDINAL1:def 12;
hence Segm n is Subset of omega by ORDINAL1:16; :: thesis: verum