This defines the empty set as an enumeration with no elements. Note that sets are a built-in concept in the HLM logic.

• https://en.wikipedia.org/wiki/Empty_set
• https://mathworld.wolfram.com/EmptySet.html
• https://proofwiki.org/wiki/Definition:Empty_Set
• https://ncatlab.org/nlab/show/empty+set
• http://metamath.tirix.org/df-nul.html
• https://leanprover-community.github.io/mathlib_docs/data/set/basic.html#set.empty_def