theorem :: TOPGEN_2:30

for X being infinite set holds card (Fin X) = card X