---

Step * 2 of Lemma prob2.2


1. [U] : Type
2. [P] : U ⟶ ℙ
3. [Q] : U ⟶ ℙ
4. x : U@i
5. Q x@i
⊢ (∃x:U. (P x)) ∨ (∃x:U. (Q x))
BY
{ (Sel 2 (D 0) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [U]  :  Type
2.  [P]  :  U  {}\mrightarrow{}  \mBbbP{}
3.  [Q]  :  U  {}\mrightarrow{}  \mBbbP{}
4.  x  :  U@i
5.  Q  x@i
\mvdash{}  (\mexists{}x:U.  (P  x))  \mvee{}  (\mexists{}x:U.  (Q  x))


By

---

Latex:
(Sel  2  (D  0)  THEN  Auto)\mcdot{}

---

Home Index