---

Step * 1 2 2 of Lemma fdl-eq-1

.....antecedent..... 
1. X : Type
2. x : Base
3. x ∈ X List List
4. x1 : ↑(∃a∈x.isaxiom(a))_b@i
⊢ dlattice-eq(X;x;[[]])
BY
{ ((Assert [[]] ∈ X List List BY
          Auto)
   THEN D 0
   THEN Unfold `dlattice-order` 0
   THEN (RWO "l_all_iff l_exists_iff" 0 THENA Auto)) }

1
1. X : Type
2. x : Base
3. x ∈ X List List
4. x1 : ↑(∃a∈x.isaxiom(a))_b@i
5. [[]] ∈ X List List
⊢ ∀b:X List. ((b ∈ [[]]) ⇒ (∃a∈x. a ⊆ b))

2
1. X : Type
2. x : Base
3. x ∈ X List List
4. x1 : ↑(∃a∈x.isaxiom(a))_b@i
5. [[]] ∈ X List List
⊢ ∀b:X List. ((b ∈ x) ⇒ (∃a∈[[]]. a ⊆ b))

---

Latex:

---

Latex:
.....antecedent..... 
1.  X  :  Type
2.  x  :  Base
3.  x  \mmember{}  X  List  List
4.  x1  :  \muparrow{}(\mexists{}a\mmember{}x.isaxiom(a))\_b@i
\mvdash{}  dlattice-eq(X;x;[[]])


By

---

Latex:
((Assert  [[]]  \mmember{}  X  List  List  BY
                Auto)
  THEN  D  0
  THEN  Unfold  `dlattice-order`  0
  THEN  (RWO  "l\_all\_iff  l\_exists\_iff"  0  THENA  Auto))

---

Home Index