Definition for LatRel and reactivation of the related theorems

[avekens]

As already discussed in #4298, there is no definition for LatRel in set.mm, and the related theorems are commented out. It should be discussed/decided if such a definition is helpful, and if these theorems in (current) subsection 9.2.6 "Posets and lattices as relations" (between ~tsrss and ~ledm) shall be activated (and probably revised).
Maybe they can/should be deleted if they are useless.
@digama0 you revised already some of these theorems in 2023 - what do you think?