---

Step * 1 of Lemma f-union-subset


1. A : Type
2. eq : EqDecider(A)
3. x : fset(A)
4. y : fset(A)
5. z : fset(A)
6. x ⊆ z
7. ∀a:A. a ∈ z supposing a ∈ y
8. a : A@i
9. a ∈ x ⋃ y
⊢ a ∈ z
BY
{ ((RWO "member-fset-union" (-1) THEN Auto) THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  eq  :  EqDecider(A)
3.  x  :  fset(A)
4.  y  :  fset(A)
5.  z  :  fset(A)
6.  x  \msubseteq{}  z
7.  \mforall{}a:A.  a  \mmember{}  z  supposing  a  \mmember{}  y
8.  a  :  A@i
9.  a  \mmember{}  x  \mcup{}  y
\mvdash{}  a  \mmember{}  z


By

---

Latex:
((RWO  "member-fset-union"  (-1)  THEN  Auto)  THEN  D  -1  THEN  Auto)

---

Home Index