theorem Th9: :: LOPCLSET:9

for T being non empty TopSpace holds LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is Lattice