let T be non empty discrete TopStruct ; :: thesis: ( SmallestPartition the carrier of T is Basis of T & ( for B being Basis of T holds SmallestPartition the carrier of T c= B ) )
set B0 = SmallestPartition the carrier of T;
A1: SmallestPartition the carrier of T = { {a} where a is Element of T : verum } by EQREL_1:46;
A2: SmallestPartition the carrier of T c= the topology of T

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in SmallestPartition the carrier of T or a in the topology of T )
assume a in SmallestPartition the carrier of T ; :: thesis: a in the topology of T
then reconsider a = a as Subset of T ;
a is open by TDLAT_3:17;
hence a in the topology of T by PRE_TOPC:def 5; :: thesis: verum

end;

now

let A be Subset of T; :: thesis: ( A is open implies for p being Point of T st p in A holds
ex a being Subset of T st
( a in SmallestPartition the carrier of T & p in a & a c= A ) )
assume A is open ; :: thesis: for p being Point of T st p in A holds
ex a being Subset of T st
( a in SmallestPartition the carrier of T & p in a & a c= A )
let p be Point of T; :: thesis: ( p in A implies ex a being Subset of T st
( a in SmallestPartition the carrier of T & p in a & a c= A ) )
assume A3: p in A ; :: thesis: ex a being Subset of T st
( a in SmallestPartition the carrier of T & p in a & a c= A )
reconsider a = {p} as Subset of T ;
take a = a; :: thesis: ( a in SmallestPartition the carrier of T & p in a & a c= A )
thus a in SmallestPartition the carrier of T by A1; :: thesis: ( p in a & a c= A )
thus p in a by TARSKI:def 1; :: thesis: a c= A
thus a c= A by A3, ZFMISC_1:37; :: thesis: verum

end;

hence A4: SmallestPartition the carrier of T is Basis of T by A2, YELLOW_9:32; :: thesis: for B being Basis of T holds SmallestPartition the carrier of T c= B
let B be Basis of T; :: thesis: SmallestPartition the carrier of T c= B
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in SmallestPartition the carrier of T or a in B )
assume A5: a in SmallestPartition the carrier of T ; :: thesis: a in B
then consider b being Element of T such that
A6: a = {b} by A1;
reconsider a = a as Subset of T by A5;
( a is open & b in a ) by A4, A5, A6, TARSKI:def 1, YELLOW_8:19;
then consider U being Subset of T such that
A7: ( U in B & b in U & U c= a ) by YELLOW_9:31;
a c= U by A6, A7, ZFMISC_1:37;
hence a in B by A7, XBOOLE_0:def 10; :: thesis: verum