---

Step * of Lemma lattice-fset-join_functionality_wrt_subset

∀[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s1,s2:fset(Point(l))].  \/(s1) ≤ \/(s2) supposing s1 ⊆ s2
BY
{ (Auto THEN (InstLemma `lattice-fset-join-is-lub` [⌜l⌝;⌜eq⌝]⋅ THENA Auto) THEN D -1 THEN BHyp -1  THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[l:BoundedLattice].  \mforall{}[eq:EqDecider(Point(l))].  \mforall{}[s1,s2:fset(Point(l))].
    \mbackslash{}/(s1)  \mleq{}  \mbackslash{}/(s2)  supposing  s1  \msubseteq{}  s2


By

---

Latex:
(Auto
  THEN  (InstLemma  `lattice-fset-join-is-lub`  [\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  BHyp  -1 
  THEN  Auto)

---

Home Index