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 } ;
A1: card { (F ` ) where F is Subset of X : F is finite } = card X by Th33;
assume A2: B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F ` ) where F is Subset of X : F is finite } ; :: thesis: card B0 = card X
A3: ( card {{x0}} = 1 & card (SmallestPartition X) = card X ) by Th13, CARD_1:50;
A4: 1 in card X by CARD_3:103;
then (card X) +` 1 = card X by CARD_3:118;
then A5: card ((SmallestPartition X) \ {{x0}}) = card X by A3, A4, CARD_3:144;
then card B0 c= (card X) +` (card X) by A1, A2, CARD_2:47;
hence card B0 c= card X by CARD_3:117; :: according to XBOOLE_0:def 10 :: thesis: card X c= card B0
thus card X c= card B0 by A2, A5, CARD_1:27, XBOOLE_1:7; :: thesis: verum