for A being Ordinal holds
( A is finite iff A in omega ) by Lm5;