let X be infinite set ; :: thesis: for x0 being set
for B0 being Basis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } holds
card B0 = card X
let x0 be set ; :: thesis: for B0 being Basis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } holds
card B0 = card X
set T = DiscrWithInfin (X,x0);
let B0 be Basis of (DiscrWithInfin (X,x0)); :: thesis: ( B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } implies card B0 = card X )
set SX = SmallestPartition X;
set FX = { (F `) where F is Subset of X : F is finite } ;
assume A1: B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } ; :: thesis: card B0 = card X
A2: card (SmallestPartition X) = card X by Th12;
A3: card {{x0}} = 1 by CARD_1:30;
A4: 1 in card X by CARD_3:86;
then (card X) +` 1 = card X by CARD_2:76;
then A5: card ((SmallestPartition X) \ {{x0}}) = card X by A3, A2, A4, CARD_2:98;
card { (F `) where F is Subset of X : F is finite } = card X by Th31;
then card B0 c= (card X) +` (card X) by A1, A5, CARD_2:34;
hence card B0 c= card X by CARD_2:75; :: according to XBOOLE_0:def 10 :: thesis: card X c= card B0
thus card X c= card B0 by A1, A5, CARD_1:11, XBOOLE_1:7; :: thesis: verum