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 : F is finite }
set T = DiscrWithInfin X,x0;
set O1 = { U where U is Subset of : not x0 in U } ;
set O2 = { (F ` ) where F is Subset of : F is finite } ;
set B1 = (SmallestPartition X) \ {{x0}};
set B2 = { (F ` ) where F is Subset of : F is finite } ;
A1: (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 A2: a in (SmallestPartition X) \ {{x0}} ; :: thesis: a in the topology of (DiscrWithInfin X,x0)
then A3: a in SmallestPartition X by 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 A4: ex x being Element of X st a = {x} by A3;
a <> {x0} by A2, ZFMISC_1:64;
then not x0 in a by A4, TARSKI:def 1;
then a is open Subset of by A2, Def5, Th21;
hence a in the topology of (DiscrWithInfin X,x0) by PRE_TOPC:def 5; :: thesis: verum

end;

A5: the carrier of (DiscrWithInfin X,x0) = X by Def5;
{ (F ` ) where F is Subset of : 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 : F is finite } or a in bool the carrier of (DiscrWithInfin X,x0) )
assume a in { (F ` ) where F is Subset of : F is finite } ; :: thesis: a in bool the carrier of (DiscrWithInfin X,x0)
then ex F being Subset of st
( a = F ` & F is finite ) ;
hence a in bool the carrier of (DiscrWithInfin X,x0) by A5; :: thesis: verum

end;

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

A6: now

let A be Subset of ; :: thesis: ( A is open implies for p being Point of st p in A holds
ex a being Subset of st
( a in B0 & p in a & a c= A ) )
assume A is open ; :: thesis: for p being Point of st p in A holds
ex a being Subset of st
( a in B0 & p in a & a c= A )
then A7: ( not x0 in A or A ` is finite ) by Th21;
let p be Point of ; :: thesis: ( p in A implies ex a being Subset of st
( a in B0 & p in a & a c= A ) )
assume A8: p in A ; :: thesis: ex a being Subset of 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 ;
( {p} <> {x0} or (A ` ) ` in { (F ` ) where F is Subset of : F is finite } ) by A5, A8, A7, ZFMISC_1:6;
then ( not {p} in {{x0}} or A in { (F ` ) where F is Subset of : F is finite } ) by TARSKI:def 1;
then ( {p} in (SmallestPartition X) \ {{x0}} or A in { (F ` ) where F is Subset of : 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 st
( a in B0 & p in a & a c= A ) by A8; :: thesis: verum

end;

{ (F ` ) where F is Subset of : 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 : F is finite } or a in the topology of (DiscrWithInfin X,x0) )
assume a in { (F ` ) where F is Subset of : F is finite } ; :: thesis: a in the topology of (DiscrWithInfin X,x0)
then consider F being Subset of such that
A10: a = F ` and
A11: F is finite ;
(F ` ) ` is finite by A11;
then a is open Subset of by A5, A10, Th21;
hence a in the topology of (DiscrWithInfin X,x0) by PRE_TOPC:def 5; :: thesis: verum

end;

then reconsider B0 = B0 as Basis of DiscrWithInfin X,x0 by A1, A6, XBOOLE_1:8, YELLOW_9:32;
take B0 ; :: thesis: B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F ` ) where F is Subset of : F is finite }
thus B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F ` ) where F is Subset of : F is finite } ; :: thesis: verum