The next several commands in set1.lp axiomatize the properties of finite sets of elements.

The set command directs LP to assign the namesset name setAxioms assert sort S generated by {}, insert; {e} = insert(e, {}); ~(e \in {}); e \in insert(e1, x) <=> e = e1 \/ e \in x; {} \subseteq x; insert(e, x) \subseteq y <=> e \in y /\ x \subseteq y; e \in (x \union y) <=> e \in x \/ e \in y .. set name extensionality assert \A e (e \in x <=> e \in y) => x = y

The axioms are formulated using declared symbols (for sorts, variables, and
operators) together with logical symbols for
equality (`=`), negation (`~`), conjunction (`/\`),
disjunction (`\/`), implication (`=>`), logical equivalence (`<=>`), and
universal quantification (`\A`). LP also provides a
symbol for existential quantification (`\E`). LP uses a limited amount of
\llink{precedence} when parsing formulas: for example, the logical operator
`<=>` binds less tightly than the other logical operators, which bind less
tightly than the equality operator, which bind less tightly than declared
operators like `\in` and `\union`.