Root element. File specification, authors, imports and so on are part of the header. File specification of this module. Title of this module. Contents description. Authors of this module. Name and email address of author. Other modules that are a precondition for this one. A module that must be imported. Prefix for labels from referenced module. References to labels in the referenced module must be extended with this prefix. Modules which use (import) this module. This information could be incorrect due to changes in the referenced modules. Also newly created modules could be missing. To keep these entries correct the external module administrator should email the module administrator of this module. Email address for administration services of this module. Chapter title. Contents description. Section. Section title. Contents description. Logical existence quantor. Logical universal quantor. Logical conjunction. Logical disjunction. Logical equivalence. Logical implication. Logical negation. This a normal LaTeX subsection of a section. Subsection title. The LaTeX text of this subsection. This part is the smallest unit and carries formulas. Short text to describe this item. Occurrs when referencing to this. Subsection title. Contents description. Contents description. Definition of predicate or term constants. A theorem and it's proof. An axiom formula. An email address. Location directory of module. Level information.