for X being set holds
( X is finite iff card X in omega ) by Th42;