for X being infinite set
for x0 being set
for B being Basis of (DiscrWithInfin (X,x0)) holds card X c= card B