---

Step * 2 of Lemma lattice-meet-eq-1


1. l : BoundedLattice
2. x : Point(l)
3. y : Point(l)
4. x ∧ y = 1 ∈ Point(l)
⊢ y = 1 ∈ Point(l)
BY
{ Assert ⌜y ∧ x = 1 ∈ Point(l)⌝⋅ }

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

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

---

Latex:

---

Latex:

1.  l  :  BoundedLattice
2.  x  :  Point(l)
3.  y  :  Point(l)
4.  x  \mwedge{}  y  =  1
\mvdash{}  y  =  1


By

---

Latex:
Assert  \mkleeneopen{}y  \mwedge{}  x  =  1\mkleeneclose{}\mcdot{}

---

Home Index