theorem Th30: :: TDLAT_1:30

for T being TopSpace holds LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is C_Lattice