for T being non empty discrete TopStruct holds
( SmallestPartition the carrier of T is Basis of T & ( for B being Basis of T holds SmallestPartition the carrier of T c= B ) )