---

Step * 1 2 1 1 1 7 1 of Lemma quotient-dl_wf


1. l : BoundedDistributiveLattice
2. eq : Point(l) ⟶ Point(l) ⟶ ℙ
3. EquivRel(Point(l);x,y.eq[x;y])
4. ∀a,c,b,d:Point(l).  (eq[a;c] ⇒ eq[b;d] ⇒ eq[a ∧ b;c ∧ d])
5. ∀a,c,b,d:Point(l).  (eq[a;c] ⇒ eq[b;d] ⇒ eq[a ∨ b;c ∨ d])
6. l."meet" ∈ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y])
7. l."join" ∈ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y]) ⟶ (x,y:Point(l)//eq[x;y])
8. ∀[a,b:Point(l)].  (a ∧ b = b ∧ a ∈ Point(l))
9. ∀[a,b:Point(l)].  (a ∨ b = b ∨ a ∈ Point(l))
10. ∀[a,b,c:Point(l)].  (a ∧ b ∧ c = a ∧ b ∧ c ∈ Point(l))
11. ∀[a,b,c:Point(l)].  (a ∨ b ∨ c = a ∨ b ∨ c ∈ Point(l))
12. ∀[a,b:Point(l)].  (a ∨ a ∧ b = a ∈ Point(l))
13. ∀[a,b:Point(l)].  (a ∧ a ∨ b = a ∈ Point(l))
14. ∀[a:Point(l)]. (a ∨ 0 = a ∈ Point(l))
15. ∀[a:Point(l)]. (a ∧ 1 = a ∈ Point(l))
16. ∀[a,b,c:Point(l)].  (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(l))
17. ∀[a,b:x,y:Point(l)//(eq x y)].  (a ∧ b ∈ x,y:Point(l)//(eq x y))
18. ∀[a,b:x,y:Point(l)//(eq x y)].  (a ∨ b ∈ x,y:Point(l)//(eq x y))
19. a : Base
20. a1 : Base
21. a = a1 ∈ pertype(λx,y. ((x ∈ Point(l)) ∧ (y ∈ Point(l)) ∧ (eq x y)))
22. a ∈ Point(l)
23. a1 ∈ Point(l)
24. eq a a1
⊢ a ∧ 1 = a1 ∈ (x,y:Point(l)//(eq x y))
BY
{ ((Assert a ∧ 1 = a ∈ (x,y:Point(l)//(eq x y)) BY
          BackThruSomeHyp)
   THEN (Assert a = a1 ∈ (x,y:Point(l)//(eq x y)) BY
               (EqTypeCD THEN Auto))
   THEN Eq) }

---

Latex:

---

Latex:

1.  l  :  BoundedDistributiveLattice
2.  eq  :  Point(l)  {}\mrightarrow{}  Point(l)  {}\mrightarrow{}  \mBbbP{}
3.  EquivRel(Point(l);x,y.eq[x;y])
4.  \mforall{}a,c,b,d:Point(l).    (eq[a;c]  {}\mRightarrow{}  eq[b;d]  {}\mRightarrow{}  eq[a  \mwedge{}  b;c  \mwedge{}  d])
5.  \mforall{}a,c,b,d:Point(l).    (eq[a;c]  {}\mRightarrow{}  eq[b;d]  {}\mRightarrow{}  eq[a  \mvee{}  b;c  \mvee{}  d])
6.  l."meet"  \mmember{}  (x,y:Point(l)//eq[x;y])  {}\mrightarrow{}  (x,y:Point(l)//eq[x;y])  {}\mrightarrow{}  (x,y:Point(l)//eq[x;y])
7.  l."join"  \mmember{}  (x,y:Point(l)//eq[x;y])  {}\mrightarrow{}  (x,y:Point(l)//eq[x;y])  {}\mrightarrow{}  (x,y:Point(l)//eq[x;y])
8.  \mforall{}[a,b:Point(l)].    (a  \mwedge{}  b  =  b  \mwedge{}  a)
9.  \mforall{}[a,b:Point(l)].    (a  \mvee{}  b  =  b  \mvee{}  a)
10.  \mforall{}[a,b,c:Point(l)].    (a  \mwedge{}  b  \mwedge{}  c  =  a  \mwedge{}  b  \mwedge{}  c)
11.  \mforall{}[a,b,c:Point(l)].    (a  \mvee{}  b  \mvee{}  c  =  a  \mvee{}  b  \mvee{}  c)
12.  \mforall{}[a,b:Point(l)].    (a  \mvee{}  a  \mwedge{}  b  =  a)
13.  \mforall{}[a,b:Point(l)].    (a  \mwedge{}  a  \mvee{}  b  =  a)
14.  \mforall{}[a:Point(l)].  (a  \mvee{}  0  =  a)
15.  \mforall{}[a:Point(l)].  (a  \mwedge{}  1  =  a)
16.  \mforall{}[a,b,c:Point(l)].    (a  \mwedge{}  b  \mvee{}  c  =  a  \mwedge{}  b  \mvee{}  a  \mwedge{}  c)
17.  \mforall{}[a,b:x,y:Point(l)//(eq  x  y)].    (a  \mwedge{}  b  \mmember{}  x,y:Point(l)//(eq  x  y))
18.  \mforall{}[a,b:x,y:Point(l)//(eq  x  y)].    (a  \mvee{}  b  \mmember{}  x,y:Point(l)//(eq  x  y))
19.  a  :  Base
20.  a1  :  Base
21.  a  =  a1
22.  a  \mmember{}  Point(l)
23.  a1  \mmember{}  Point(l)
24.  eq  a  a1
\mvdash{}  a  \mwedge{}  1  =  a1


By

---

Latex:
((Assert  a  \mwedge{}  1  =  a  BY  BackThruSomeHyp)  THEN  (Assert  a  =  a1  BY  (EqTypeCD  THEN  Auto))  THEN  Eq)

---

Home Index