for T being non empty TopSpace holds LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is Lattice