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 Th31;
card B0 = card X by A1, Th34;
hence weight (DiscrWithInfin X,x0) c= card X by WAYBEL23:74; :: 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:75;
hence card X c= weight (DiscrWithInfin X,x0) by Th35; :: thesis: verum