Restructure part 9

[zwang123]

#4253

Changes

• Moved: codu to odubas -> top
• Moved: pospropd to oduposb -> after isposix
• Moved: meet0 to odujoin and poslubmo  to posglbd -> after meetcom
• Moved: odulatb and odulat -> after islat
• Moved: oduclatb -> after clatglbcl2 
• Renamed: posglbd -> posglbdg
• Moved: The distributive lattice of sets under inclusion -> after distributive lattices
• Moved: latmass to latdisd -> lattice section
• Reversed order for join0 and meet0 and for odu*, for consistency
• Added tosets and complete lattices section
• Changed other sections based on BJ's proposal (directed set and proset could be separated but the sections would become very short so I am not doing it now...)
• etc

[avekens]

Looks fine for now. Let's see how it looks in HTML. Maybe we need some finetuning then.

[benjub]

Which ones ?

[avekens]

Currently, there is no definition for LatRel in set.mm, and the related theorems are commented out. Maybe a separate issue should be created to revise and activate all these theorems in (current) subsection 9.2.6 "Posets and lattices as relations" (between ~tsrss and ~ledm). Or they should be deleted if they are useless. @digama0 you revised already some of these theorems in 2023 - what do you think?

Nevertheless, I will merge this PR now (to see how the new structure will show up in HTML), because there are 4 approvals.

[avekens]

Currently, there is no definition for LatRel in set.mm, and the related theorems are commented out. Maybe a separate issue should be created to revise and activate all these theorems in (current) subsection 9.2.6 "Posets and lattices as relations" (between ~tsrss and ~ledm). Or they should be deleted if they are useless.

Issue #4302 opened for this topic.