theorem Th3: :: OPENLATT:3

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