let a be set ; :: thesis: ( a is natural implies a is finite )
assume a in omega ; :: according to ORDINAL1:def 13 :: thesis: a is finite
hence a is finite ; :: thesis: verum