let n be number ; :: thesis: ( n is natural implies n is ordinal )
assume n is natural ; :: thesis: n is ordinal
then reconsider n = n as Element of omega by Def13;
n is ordinal ;
hence n is ordinal ; :: thesis: verum