The next three theorems in set1.lp follow from the principle of extensionality.

The instantiate command directs LP to form the substitution instanceprove x \union {} = x instantiate y by x \union {} in extensionality qed

of the fact name\A e (e \in x <=> e \in x \union {}) => x = x \union {}

using the definition of\A e (e \in x <=> e \in x \/ e \in {}) => x = x \union {}

using the definition of\A e (e \in x <=> e \in x \/ false) => x = x \union {}

using LP's hardwired axioms. LP orients this final simplification into the rewrite rule\A e (e \in x <=> e \in x) => x = x \union {} \A e (true) => x = x \union {} true => x = x \union {} x = x \union {}

Two other theorems about union can also be proved by instantiating the extensionality axiom. Both proofs are left as exercises to the reader.

prove x \union insert(e, y) = insert(e, x \union y) prove ac \union