let n be number ; :: thesis: ( n is finite & n is ordinal implies n is natural )
assume ( n is finite & n is ordinal ) ; :: thesis: n is natural
then n in omega by Lm4;
hence n is natural ; :: thesis: verum