let X be infinite set ; :: thesis: for x0 being set holds weight (DiscrWithInfin (X,x0)) = card X
let x0 be set ; :: thesis: weight (DiscrWithInfin (X,x0)) = card X
set T = DiscrWithInfin (X,x0);
consider B0 being Basis of (DiscrWithInfin (X,x0)) such that
A1: B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } by Th29;
card B0 = card X by A1, Th32;
hence weight (DiscrWithInfin (X,x0)) c= card X by WAYBEL23:73; :: according to XBOOLE_0:def 10 :: thesis: card X c= weight (DiscrWithInfin (X,x0))
ex B being Basis of (DiscrWithInfin (X,x0)) st card B = weight (DiscrWithInfin (X,x0)) by WAYBEL23:74;
hence card X c= weight (DiscrWithInfin (X,x0)) by Th33; :: thesis: verum