let X be infinite set ; :: thesis: for x0 being set
for B being Basis of DiscrWithInfin X,x0 holds card X c= card B
let x0 be set ; :: thesis: for B being Basis of DiscrWithInfin X,x0 holds card X c= card B
set T = DiscrWithInfin X,x0;
A1: the carrier of (DiscrWithInfin X,x0) = X by Def5;
set SX = SmallestPartition X;
A2: ( card {{x0}} = 1 & card (SmallestPartition X) = card X ) by Th13, CARD_1:50;
A3: 1 in card X by CARD_3:103;
then (card X) +` 1 = card X by CARD_3:118;
then A4: card ((SmallestPartition X) \ {{x0}}) = card X by A2, A3, CARD_3:144;
A5: SmallestPartition X = { {x} where x is Element of X : verum } by EQREL_1:46;
let B be Basis of DiscrWithInfin X,x0; :: thesis: card X c= card B
(SmallestPartition X) \ {{x0}} c= B

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (SmallestPartition X) \ {{x0}} or a in B )
assume a in (SmallestPartition X) \ {{x0}} ; :: thesis: a in B
then ( a in SmallestPartition X & not a in {{x0}} ) by XBOOLE_0:def 5;
then ( ex x being Element of X st a = {x} & a <> {x0} ) by A5, TARSKI:def 1;
then consider x being Element of (DiscrWithInfin X,x0) such that
A6: ( a = {x} & x <> x0 ) by A1;
( x in a & a is open Subset of (DiscrWithInfin X,x0) ) by A1, A6, Th24, TARSKI:def 1;
then consider U being Subset of (DiscrWithInfin X,x0) such that
A7: ( U in B & x in U & U c= a ) by YELLOW_9:31;
a = U

proof

thus a c= U by A6, A7, ZFMISC_1:37; :: according to XBOOLE_0:def 10 :: thesis: U c= a
thus U c= a by A7; :: thesis: verum

end;

hence a in B by A7; :: thesis: verum

end;

hence card X c= card B by A4, CARD_1:27; :: thesis: verum