let o be natural Number ; :: thesis: o is ordinal
o in omega by ORDINAL1:def 12;
hence o is ordinal ; :: thesis: verum