---

Step * 1 1 of Lemma dlattice-order-append


1. X : Type
2. a1 : X List List
3. b1 : X List List
4. a2 : X List List
5. b2 : X List List
6. (∀b∈b1.(∃a∈a1. b ⊆ a))
7. (∀b∈b2.(∃a∈a2. b ⊆ a))
⊢ (∀b∈b1.(∃a∈a1. b ⊆ a) ∨ (∃a∈a2. b ⊆ a))
BY
{ (RepeatFor 2 (ParallelOp -2) THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  a1  :  X  List  List
3.  b1  :  X  List  List
4.  a2  :  X  List  List
5.  b2  :  X  List  List
6.  (\mforall{}b\mmember{}b1.(\mexists{}a\mmember{}a1.  b  \msubseteq{}  a))
7.  (\mforall{}b\mmember{}b2.(\mexists{}a\mmember{}a2.  b  \msubseteq{}  a))
\mvdash{}  (\mforall{}b\mmember{}b1.(\mexists{}a\mmember{}a1.  b  \msubseteq{}  a)  \mvee{}  (\mexists{}a\mmember{}a2.  b  \msubseteq{}  a))


By

---

Latex:
(RepeatFor  2  (ParallelOp  -2)  THEN  Auto)

---

Home Index