theorem :: TOPGEN_2:34

for X being infinite set
for x0 being set holds weight (DiscrWithInfin (X,x0)) = card X