---

Step * 2 1 of Lemma fset-ac-le-distributive


1. T : Type
2. eq : EqDecider(T)
3. a : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
4. b : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
5. c : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
⊢ fset-ac-le(eq;fset-ac-glb(eq;a;c);fset-ac-lub(eq;b;c))
BY
{ (Using [`ac2',⌜c⌝] (BLemma `fset-ac-le_transitivity`)⋅
   THEN Auto
   THEN (InstLemma `fset-ac-glb-is-glb` [⌜T⌝;⌜eq⌝;⌜a⌝;⌜c⌝]⋅ THEN Auto)
   THEN InstLemma `fset-ac-lub-is-lub` [⌜T⌝;⌜eq⌝;⌜b⌝;⌜c⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  a  :  \{ac:fset(fset(T))|  \muparrow{}fset-antichain(eq;ac)\} 
4.  b  :  \{ac:fset(fset(T))|  \muparrow{}fset-antichain(eq;ac)\} 
5.  c  :  \{ac:fset(fset(T))|  \muparrow{}fset-antichain(eq;ac)\} 
\mvdash{}  fset-ac-le(eq;fset-ac-glb(eq;a;c);fset-ac-lub(eq;b;c))


By

---

Latex:
(Using  [`ac2',\mkleeneopen{}c\mkleeneclose{}]  (BLemma  `fset-ac-le\_transitivity`)\mcdot{}
  THEN  Auto
  THEN  (InstLemma  `fset-ac-glb-is-glb`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  InstLemma  `fset-ac-lub-is-lub`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index