---

Step * of Lemma bounded-lattice-hom-equal

∀[l1,l2:BoundedLatticeStructure]. ∀[f,g:Hom(l1;l2)].
  f = g ∈ Hom(l1;l2) supposing ∀x:Point(l1). ((f x) = (g x) ∈ Point(l2))
BY
{ (Auto THEN RepeatFor 2 ((DVar `f' THEN EqTypeCD THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[l1,l2:BoundedLatticeStructure].  \mforall{}[f,g:Hom(l1;l2)].    f  =  g  supposing  \mforall{}x:Point(l1).  ((f  x)  =  (g  x))


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((DVar  `f'  THEN  EqTypeCD  THEN  Auto)))

---

Home Index