---

Step * of Lemma lattice-meet-eq-1

No Annotations
∀[l:BoundedLattice]. ∀[x,y:Point(l)].  uiff(x ∧ y = 1 ∈ Point(l);(x = 1 ∈ Point(l)) ∧ (y = 1 ∈ Point(l)))
BY
{ Auto }

1
1. l : BoundedLattice
2. x : Point(l)
3. y : Point(l)
4. x ∧ y = 1 ∈ Point(l)
⊢ x = 1 ∈ Point(l)

2
1. l : BoundedLattice
2. x : Point(l)
3. y : Point(l)
4. x ∧ y = 1 ∈ Point(l)
⊢ y = 1 ∈ Point(l)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[l:BoundedLattice].  \mforall{}[x,y:Point(l)].    uiff(x  \mwedge{}  y  =  1;(x  =  1)  \mwedge{}  (y  =  1))


By

---

Latex:
Auto

---

Home Index