---

Step * 1 of Lemma lattice-1-le-iff


1. l : BoundedLattice
2. b : Point(l)
⊢ uiff(b = 1 ∨ b ∈ Point(l);b = 1 ∈ Point(l))
BY
{ (RWO "lattice-join-1" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  l  :  BoundedLattice
2.  b  :  Point(l)
\mvdash{}  uiff(b  =  1  \mvee{}  b;b  =  1)


By

---

Latex:
(RWO  "lattice-join-1"  0  THEN  Auto)

---

Home Index