let X, x0 be set ; :: thesis: 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 O1 = { U where U is Subset of X : not x0 in U } ;
set O2 = { (F ` ) where F is Subset of X : F is finite } ;
A1: ( the carrier of (DiscrWithInfin X,x0) = X & the topology of (DiscrWithInfin X,x0) = { U where U is Subset of X : not x0 in U } \/ { (F ` ) where F is Subset of X : F is finite } ) by Def5;
set B1 = (SmallestPartition X) \ {{x0}};
set B2 = { (F ` ) where F is Subset of X : F is finite } ;
{ (F ` ) where F is Subset of X : F is finite } c= bool the carrier of (DiscrWithInfin X,x0)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (F ` ) where F is Subset of X : F is finite } or a in bool the carrier of (DiscrWithInfin X,x0) )
assume a in { (F ` ) where F is Subset of X : F is finite } ; :: thesis: a in bool the carrier of (DiscrWithInfin X,x0)
then ex F being Subset of X st
( a = F ` & F is finite ) ;
hence a in bool the carrier of (DiscrWithInfin X,x0) by A1; :: thesis: verum

end;

then reconsider B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F ` ) where F is Subset of X : F is finite } as Subset-Family of (DiscrWithInfin X,x0) by A1, XBOOLE_1:8;
A2: (SmallestPartition X) \ {{x0}} c= the topology of (DiscrWithInfin X,x0)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (SmallestPartition X) \ {{x0}} or a in the topology of (DiscrWithInfin X,x0) )
assume A3: a in (SmallestPartition X) \ {{x0}} ; :: thesis: a in the topology of (DiscrWithInfin X,x0)
then A4: ( a is Subset of (DiscrWithInfin X,x0) & a in SmallestPartition X & a <> {x0} ) by Def5, ZFMISC_1:64;
then reconsider X = X as non empty set by EQREL_1:41;
SmallestPartition X = { {x} where x is Element of X : verum } by EQREL_1:46;
then ex x being Element of X st a = {x} by A4;
then not x0 in a by A4, TARSKI:def 1;
then a is open Subset of (DiscrWithInfin X,x0) by A3, Def5, Th21;
hence a in the topology of (DiscrWithInfin X,x0) by PRE_TOPC:def 5; :: thesis: verum

end;

B6: { (F ` ) where F is Subset of X : F is finite } c= the topology of (DiscrWithInfin X,x0)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (F ` ) where F is Subset of X : F is finite } or a in the topology of (DiscrWithInfin X,x0) )
assume a in { (F ` ) where F is Subset of X : F is finite } ; :: thesis: a in the topology of (DiscrWithInfin X,x0)
then consider F being Subset of X such that
A5: ( a = F ` & F is finite ) ;
(F ` ) ` is finite by A5;
then a is open Subset of (DiscrWithInfin X,x0) by A1, A5, Th21;
hence a in the topology of (DiscrWithInfin X,x0) by PRE_TOPC:def 5; :: thesis: verum

end;

now

let A be Subset of (DiscrWithInfin X,x0); :: thesis: ( 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 A7: A is open ; :: thesis: 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 p be Point of (DiscrWithInfin X,x0); :: thesis: ( 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 ; :: thesis: ex a being Subset of (DiscrWithInfin X,x0) st
( a in B0 & p in a & a c= A )
reconsider X' = X as non empty set by A8, Def5;
reconsider p' = p as Element of X' by Def5;
SmallestPartition X = { {x} where x is Element of X' : verum } by EQREL_1:46;
then A9: {p'} in SmallestPartition X ;
( not x0 in A or A ` is finite ) by A7, Th21;
then ( {p} <> {x0} or (A ` ) ` in { (F ` ) where F is Subset of X : F is finite } ) by A1, A8, ZFMISC_1:6;
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:37;
hence ex a being Subset of (DiscrWithInfin X,x0) st
( a in B0 & p in a & a c= A ) by A8; :: thesis: verum

end;

then reconsider B0 = B0 as Basis of DiscrWithInfin X,x0 by B6, A2, XBOOLE_1:8, YELLOW_9:32;
take B0 ; :: thesis: 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 } ; :: thesis: verum