for X being set holds
( not X is finite iff ex Y being set st
( Y c= X & card Y = omega ) )