---

Step * of Lemma fdl-1-join-irreducible

∀[X:Type]
  ∀x,y:Point(free-dl(X)).  (x ∨ y = 1 ∈ Point(free-dl(X)) ⇐⇒ (x = 1 ∈ Point(free-dl(X))) ∨ (y = 1 ∈ Point(free-dl(X))))
BY
{ Auto }

1
1. [X] : Type
2. x : Point(free-dl(X))
3. y : Point(free-dl(X))
4. x ∨ y = 1 ∈ Point(free-dl(X))
⊢ (x = 1 ∈ Point(free-dl(X))) ∨ (y = 1 ∈ Point(free-dl(X)))

2
1. X : Type
2. x : Point(free-dl(X))
3. y : Point(free-dl(X))
4. (x = 1 ∈ Point(free-dl(X))) ∨ (y = 1 ∈ Point(free-dl(X)))
⊢ x ∨ y = 1 ∈ Point(free-dl(X))

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}x,y:Point(free-dl(X)).    (x  \mvee{}  y  =  1  \mLeftarrow{}{}\mRightarrow{}  (x  =  1)  \mvee{}  (y  =  1))


By

---

Latex:
Auto

---

Home Index