# LP, the Larch Prover -- Sample proofs: two final theorems about subset

The new induction rule, setTheorems.9, helps us prove the following theorem about subsets:
```prove x \subseteq (x \union y) by induction on x using setTheorems
qed
```
The prove command directs LP to use the induction rule just proved to formulate subgoals for the proof by induction using the generators {}, {__}, and \union instead of the generators {} and insert:
```Creating subgoals for proof by structural induction on `x'
Basis subgoals:
Subgoal 1: {} \subseteq ({} \union y)
Subgoal 2: {e} \subseteq ({e} \union y)
Induction constants: xc, xc1
Induction hypotheses:
setTheoremsInductHyp.1: xc \subseteq (xc \union y)
setTheoremsInductHyp.2: xc1 \subseteq (xc1 \union y)
Induction subgoal:
Subgoal 3: (xc \union xc1) \subseteq (xc1 \union xc \union y)
```
LP establishes all three subgoals automatically.

Finally, we prove the last theorem by directing LP to compute a critical pair between the theorem just established and an earlier theorem, x \union {} = x.

```prove x \subseteq x
critical-pairs setTheorems with setTheorems
qed
```