theorem :: CARD_3:87

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