---

Step * of Lemma lattice-axioms-from-order

∀[l:LatticeStructure]
  lattice-axioms(l) 
  supposing ∃R:Point(l) ⟶ Point(l) ⟶ ℙ
             (((∀[a,b:Point(l)].  least-upper-bound(Point(l);x,y.R[x;y];a;b;a ∨ b))
             ∧ (∀[a,b:Point(l)].  greatest-lower-bound(Point(l);x,y.R[x;y];a;b;a ∧ b)))
             ∧ Order(Point(l);x,y.R[x;y]))
BY
{ (((Auto THEN ExRepD) THEN D 0) THEN Auto) }

1
1. l : LatticeStructure
2. R : Point(l) ⟶ Point(l) ⟶ ℙ
3. ∀[a,b:Point(l)].  least-upper-bound(Point(l);x,y.R[x;y];a;b;a ∨ b)
4. ∀[a,b:Point(l)].  greatest-lower-bound(Point(l);x,y.R[x;y];a;b;a ∧ b)
5. Order(Point(l);x,y.R[x;y])
6. a : Point(l)
7. b : Point(l)
⊢ a ∧ b = b ∧ a ∈ Point(l)

2
1. l : LatticeStructure
2. R : Point(l) ⟶ Point(l) ⟶ ℙ
3. ∀[a,b:Point(l)].  least-upper-bound(Point(l);x,y.R[x;y];a;b;a ∨ b)
4. ∀[a,b:Point(l)].  greatest-lower-bound(Point(l);x,y.R[x;y];a;b;a ∧ b)
5. Order(Point(l);x,y.R[x;y])
6. a : Point(l)
7. b : Point(l)
⊢ a ∨ b = b ∨ a ∈ Point(l)

3
1. l : LatticeStructure
2. R : Point(l) ⟶ Point(l) ⟶ ℙ
3. ∀[a,b:Point(l)].  least-upper-bound(Point(l);x,y.R[x;y];a;b;a ∨ b)
4. ∀[a,b:Point(l)].  greatest-lower-bound(Point(l);x,y.R[x;y];a;b;a ∧ b)
5. Order(Point(l);x,y.R[x;y])
6. ∀[a,b:Point(l)].  (a ∨ b = b ∨ a ∈ Point(l))
7. a : Point(l)
8. b : Point(l)
9. c : Point(l)
⊢ a ∧ b ∧ c = a ∧ b ∧ c ∈ Point(l)

4
1. l : LatticeStructure
2. R : Point(l) ⟶ Point(l) ⟶ ℙ
3. ∀[a,b:Point(l)].  least-upper-bound(Point(l);x,y.R[x;y];a;b;a ∨ b)
4. ∀[a,b:Point(l)].  greatest-lower-bound(Point(l);x,y.R[x;y];a;b;a ∧ b)
5. Order(Point(l);x,y.R[x;y])
6. ∀[a,b:Point(l)].  (a ∨ b = b ∨ a ∈ Point(l))
7. ∀[a,b,c:Point(l)].  (a ∧ b ∧ c = a ∧ b ∧ c ∈ Point(l))
8. a : Point(l)
9. b : Point(l)
10. c : Point(l)
⊢ a ∨ b ∨ c = a ∨ b ∨ c ∈ Point(l)

5
1. l : LatticeStructure
2. R : Point(l) ⟶ Point(l) ⟶ ℙ
3. ∀[a,b:Point(l)].  least-upper-bound(Point(l);x,y.R[x;y];a;b;a ∨ b)
4. ∀[a,b:Point(l)].  greatest-lower-bound(Point(l);x,y.R[x;y];a;b;a ∧ b)
5. Order(Point(l);x,y.R[x;y])
6. ∀[a,b:Point(l)].  (a ∨ b = b ∨ a ∈ Point(l))
7. ∀[a,b,c:Point(l)].  (a ∧ b ∧ c = a ∧ b ∧ c ∈ Point(l))
8. ∀[a,b,c:Point(l)].  (a ∨ b ∨ c = a ∨ b ∨ c ∈ Point(l))
9. a : Point(l)
10. b : Point(l)
⊢ a ∨ a ∧ b = a ∈ Point(l)

6
1. l : LatticeStructure
2. R : Point(l) ⟶ Point(l) ⟶ ℙ
3. ∀[a,b:Point(l)].  least-upper-bound(Point(l);x,y.R[x;y];a;b;a ∨ b)
4. ∀[a,b:Point(l)].  greatest-lower-bound(Point(l);x,y.R[x;y];a;b;a ∧ b)
5. Order(Point(l);x,y.R[x;y])
6. ∀[a,b:Point(l)].  (a ∨ b = b ∨ a ∈ Point(l))
7. ∀[a,b,c:Point(l)].  (a ∧ b ∧ c = a ∧ b ∧ c ∈ Point(l))
8. ∀[a,b,c:Point(l)].  (a ∨ b ∨ c = a ∨ b ∨ c ∈ Point(l))
9. ∀[a,b:Point(l)].  (a ∨ a ∧ b = a ∈ Point(l))
10. a : Point(l)
11. b : Point(l)
⊢ a ∧ a ∨ b = a ∈ Point(l)

---

Latex:

---

Latex:
\mforall{}[l:LatticeStructure]
    lattice-axioms(l) 
    supposing  \mexists{}R:Point(l)  {}\mrightarrow{}  Point(l)  {}\mrightarrow{}  \mBbbP{}
                          (((\mforall{}[a,b:Point(l)].    least-upper-bound(Point(l);x,y.R[x;y];a;b;a  \mvee{}  b))
                          \mwedge{}  (\mforall{}[a,b:Point(l)].    greatest-lower-bound(Point(l);x,y.R[x;y];a;b;a  \mwedge{}  b)))
                          \mwedge{}  Order(Point(l);x,y.R[x;y]))


By

---

Latex:
(((Auto  THEN  ExRepD)  THEN  D  0)  THEN  Auto)

---

Home Index