---

Step * of Lemma lattice-1-le-iff

∀[l:BoundedLattice]. ∀[b:Point(l)].  uiff(1 ≤ b;b = 1 ∈ Point(l))
BY
{ ((UnivCD THENA Auto) THEN (RWO "lattice-le-iff" 0 THENA Auto)) }

1
1. l : BoundedLattice
2. b : Point(l)
⊢ uiff(b = 1 ∨ b ∈ Point(l);b = 1 ∈ Point(l))

---

Latex:

---

Latex:
\mforall{}[l:BoundedLattice].  \mforall{}[b:Point(l)].    uiff(1  \mleq{}  b;b  =  1)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "lattice-le-iff"  0  THENA  Auto))

---

Home Index