---

Step * of Lemma lattice-le-order

∀l:Lattice. Order(Point(l);x,y.x ≤ y)
BY
{ (Auto THEN RepeatFor 2 ((D 0 THEN Auto))) }

1
1. l : Lattice@i'
2. a : Point(l)@i
⊢ a ≤ a

2
1. l : Lattice@i'
2. a : Point(l)@i
3. b : Point(l)@i
4. c : Point(l)@i
5. a ≤ b@i
6. b ≤ c@i
⊢ a ≤ c

3
1. l : Lattice@i'
2. Trans(Point(l);x,y.x ≤ y)
3. x : Point(l)@i
4. y : Point(l)@i
5. x ≤ y@i
6. y ≤ x@i
⊢ x = y ∈ Point(l)

---

Latex:

---

Latex:
\mforall{}l:Lattice.  Order(Point(l);x,y.x  \mleq{}  y)


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index