---

Step * 1 of Lemma dlattice-order-iff


1. [X] : Type
2. as : X List List
3. bs : X List List
4. as ⇒ bs
5. x : X List
6. (x ∈ bs)
⊢ ∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x))
BY
{ (Unfold `dlattice-order` 4 THEN (RWO "l_all_iff" 4 THENA Auto) THEN (InstHyp [⌜x⌝] 4⋅ THENA Auto)) }

1
1. [X] : Type
2. as : X List List
3. bs : X List List
4. ∀b:X List. ((b ∈ bs) ⇒ (∃a∈as. a ⊆ b))
5. x : X List
6. (x ∈ bs)
7. (∃a∈as. a ⊆ x)
⊢ ∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x))

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  as  :  X  List  List
3.  bs  :  X  List  List
4.  as  {}\mRightarrow{}  bs
5.  x  :  X  List
6.  (x  \mmember{}  bs)
\mvdash{}  \mexists{}y:X  List.  ((y  \mmember{}  as)  \mwedge{}  l\_subset(X;y;x))


By

---

Latex:
(Unfold  `dlattice-order`  4  THEN  (RWO  "l\_all\_iff"  4  THENA  Auto)  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  4\mcdot{}  THENA  Auto))

---

Home Index