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 c= the topology of T
proof
let a be object ; :: 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:15;
hence a in the topology of T ; :: thesis: verum
end;
A2: SmallestPartition the carrier of T = { {a} where a is Element of T : verum } by EQREL_1:37;
now :: thesis: for A being Subset of T st A is open holds
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 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 A2; :: 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:31; :: thesis: verum
end;
hence A4: SmallestPartition the carrier of T is Basis of T by A1, 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 object ; :: 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 A2;
reconsider a = a as Subset of T by A5;
A7: b in a by A6, TARSKI:def 1;
a is open by A4, A5, YELLOW_8:10;
then consider U being Subset of T such that
A8: U in B and
A9: b in U and
A10: U c= a by A7, YELLOW_9:31;
a c= U by A6, A9, ZFMISC_1:31;
hence a in B by A8, A10, XBOOLE_0:def 10; :: thesis: verum