theorem Th38: :: TDLAT_1:38

for T being TopSpace holds LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is B_Lattice