let X, x0 be set ; ex B0 being Basis of (DiscrWithInfin (X,x0)) st B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite }
set T = DiscrWithInfin (X,x0);
set B1 = (SmallestPartition X) \ {{x0}};
set B2 = { (F `) where F is Subset of X : F is finite } ;
A1:
(SmallestPartition X) \ {{x0}} c= the topology of (DiscrWithInfin (X,x0))
A5:
the carrier of (DiscrWithInfin (X,x0)) = X
by Def5;
{ (F `) where F is Subset of X : F is finite } c= bool the carrier of (DiscrWithInfin (X,x0))
then reconsider B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite } as Subset-Family of (DiscrWithInfin (X,x0)) by A5, XBOOLE_1:8;
A6:
now for A being Subset of (DiscrWithInfin (X,x0)) st A is open holds
for p being Point of (DiscrWithInfin (X,x0)) st p in A holds
ex a being Subset of (DiscrWithInfin (X,x0)) st
( a in B0 & p in a & a c= A )let A be
Subset of
(DiscrWithInfin (X,x0));
( A is open implies for p being Point of (DiscrWithInfin (X,x0)) st p in A holds
ex a being Subset of (DiscrWithInfin (X,x0)) st
( a in B0 & p in a & a c= A ) )assume
A is
open
;
for p being Point of (DiscrWithInfin (X,x0)) st p in A holds
ex a being Subset of (DiscrWithInfin (X,x0)) st
( a in B0 & p in a & a c= A )then A7:
( not
x0 in A or
A ` is
finite )
by Th19;
let p be
Point of
(DiscrWithInfin (X,x0));
( p in A implies ex a being Subset of (DiscrWithInfin (X,x0)) st
( a in B0 & p in a & a c= A ) )assume A8:
p in A
;
ex a being Subset of (DiscrWithInfin (X,x0)) st
( a in B0 & p in a & a c= A )reconsider X9 =
X as non
empty set by A8, Def5;
reconsider p9 =
p as
Element of
X9 by Def5;
SmallestPartition X = { {x} where x is Element of X9 : verum }
by EQREL_1:37;
then A9:
{p9} in SmallestPartition X
;
(
{p} <> {x0} or
(A `) ` in { (F `) where F is Subset of X : F is finite } )
by A5, A8, A7, ZFMISC_1:3;
then
( not
{p} in {{x0}} or
A in { (F `) where F is Subset of X : F is finite } )
by TARSKI:def 1;
then
(
{p} in (SmallestPartition X) \ {{x0}} or
A in { (F `) where F is Subset of X : F is finite } )
by A9, XBOOLE_0:def 5;
then
( (
{p} in B0 &
p in {p} &
{p} c= A ) or (
A in B0 &
A c= A ) )
by A8, XBOOLE_0:def 3, ZFMISC_1:31;
hence
ex
a being
Subset of
(DiscrWithInfin (X,x0)) st
(
a in B0 &
p in a &
a c= A )
by A8;
verum end;
{ (F `) where F is Subset of X : F is finite } c= the topology of (DiscrWithInfin (X,x0))
then reconsider B0 = B0 as Basis of (DiscrWithInfin (X,x0)) by A1, A6, XBOOLE_1:8, YELLOW_9:32;
take
B0
; B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite }
thus
B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F `) where F is Subset of X : F is finite }
; verum