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 Nat such that
A1: A,n are_equipotent by Lm3;
A = n by A1, Lm4;
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