let A be Ordinal; :: thesis: ( A is finite iff A in omega )
thus ( A is finite implies A in omega ) :: thesis: ( A in omega implies A is finite )

proof

assume A is finite ; :: thesis: A in omega
then consider n being natural number such that
A1: A,n are_equipotent by Th74;
A = n by A1, Lm3;
hence A in omega by ORDINAL1:def 12; :: thesis: verum

end;

assume A in omega ; :: thesis: A is finite
hence A is finite ; :: thesis: verum