let X be infinite set ; for x0 being set
for B being Basis of (DiscrWithInfin (X,x0)) holds card X c= card B
let x0 be set ; for B being Basis of (DiscrWithInfin (X,x0)) holds card X c= card B
set T = DiscrWithInfin (X,x0);
set SX = SmallestPartition X;
A1:
card {{x0}} = 1
by CARD_1:30;
A2:
card (SmallestPartition X) = card X
by Th12;
let B be Basis of (DiscrWithInfin (X,x0)); card X c= card B
A3:
the carrier of (DiscrWithInfin (X,x0)) = X
by Def5;
A4:
SmallestPartition X = { {x} where x is Element of X : verum }
by EQREL_1:37;
A5:
(SmallestPartition X) \ {{x0}} c= B
proof
let a be
object ;
TARSKI:def 3 ( not a in (SmallestPartition X) \ {{x0}} or a in B )
reconsider aa =
a as
set by TARSKI:1;
assume A6:
a in (SmallestPartition X) \ {{x0}}
;
a in B
then
not
a in {{x0}}
by XBOOLE_0:def 5;
then A7:
a <> {x0}
by TARSKI:def 1;
a in SmallestPartition X
by A6, XBOOLE_0:def 5;
then
ex
x being
Element of
X st
a = {x}
by A4;
then consider x being
Element of
(DiscrWithInfin (X,x0)) such that A8:
a = {x}
and A9:
x <> x0
by A3, A7;
A10:
x in aa
by A8, TARSKI:def 1;
a is
open Subset of
(DiscrWithInfin (X,x0))
by A3, A8, A9, Th22;
then consider U being
Subset of
(DiscrWithInfin (X,x0)) such that A11:
U in B
and A12:
x in U
and A13:
U c= aa
by A10, YELLOW_9:31;
aa c= U
by A8, A12, ZFMISC_1:31;
hence
a in B
by A11, A13, XBOOLE_0:def 10;
verum
end;
A14:
1 in card X
by CARD_3:86;
then
(card X) +` 1 = card X
by CARD_2:76;
then
card ((SmallestPartition X) \ {{x0}}) = card X
by A1, A2, A14, CARD_2:98;
hence
card X c= card B
by A5, CARD_1:11; verum