---

Step * of Lemma fset-ac-lub-covers

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ]. ∀[a:fset(T)].
  (((↑ac-covers(eq;x;a)) ∨ (↑ac-covers(eq;y;a))) ⇒ (↑ac-covers(eq;fset-ac-lub(eq;x;y);a)))
BY
{ (Auto
   THEN (InstLemma `fset-minimals-ac-le` [⌜T⌝;⌜eq⌝;⌜x ⋃ y⌝]⋅ THENA Auto)
   THEN (RWO "fset-ac-le-iff" (-1) THENA Auto)
   THEN (All (RWO "assert-ac-covers") THENA Auto)
   THEN D -2
   THEN SqExRepD
   THEN (InstHyp [⌜y1⌝] (-1)⋅ THENA (Auto THEN BLemma `member-fset-union` THEN Auto))
   THEN RepeatFor 2 (ParallelLast)
   THEN Auto
   THEN InstLemma `f-subset_transitivity` [⌜T⌝;⌜eq⌝;⌜b⌝;⌜y1⌝;⌜a⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x,y:\{ac:fset(fset(T))|  \muparrow{}fset-antichain(eq;ac)\}  ].  \mforall{}[a:fset(T)].
    (((\muparrow{}ac-covers(eq;x;a))  \mvee{}  (\muparrow{}ac-covers(eq;y;a)))  {}\mRightarrow{}  (\muparrow{}ac-covers(eq;fset-ac-lub(eq;x;y);a)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `fset-minimals-ac-le`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}x  \mcup{}  y\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "fset-ac-le-iff"  (-1)  THENA  Auto)
  THEN  (All  (RWO  "assert-ac-covers")  THENA  Auto)
  THEN  D  -2
  THEN  SqExRepD
  THEN  (InstHyp  [\mkleeneopen{}y1\mkleeneclose{}]  (-1)\mcdot{}  THENA  (Auto  THEN  BLemma  `member-fset-union`  THEN  Auto))
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Auto
  THEN  InstLemma  `f-subset\_transitivity`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}y1\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index