---

Step * of Lemma fset-ac-le_transitivity

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ac1,ac2,ac3:fset(fset(T))].
  (fset-ac-le(eq;ac1;ac3)) supposing (fset-ac-le(eq;ac1;ac2) and fset-ac-le(eq;ac2;ac3))
BY
{ ((Unfold `fset-ac-le` 0 THEN Auto)
   THEN (InstLemma `fset-all-iff` [⌜fset(T)⌝;⌜deq-fset(eq)⌝]⋅ THENA Auto)
   THEN (RWW "8" 0 THENA Auto)
   THEN (RWW "8" 7 THENA Auto)
   THEN (RWW "8" 6 THENA Auto)
   THEN Thin 8) }

1
1. T : Type
2. eq : EqDecider(T)
3. ac1 : fset(fset(T))
4. ac2 : fset(fset(T))
5. ac3 : fset(fset(T))
6. ∀[x:fset(T)]. ↑¬bfset-null({y ∈ ac3 | deq-f-subset(eq) y x}) supposing x ∈ ac2
7. ∀[x:fset(T)]. ↑¬bfset-null({y ∈ ac2 | deq-f-subset(eq) y x}) supposing x ∈ ac1
⊢ ∀[x:fset(T)]. ↑¬bfset-null({y ∈ ac3 | deq-f-subset(eq) y x}) supposing x ∈ ac1

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[ac1,ac2,ac3:fset(fset(T))].
    (fset-ac-le(eq;ac1;ac3))  supposing  (fset-ac-le(eq;ac1;ac2)  and  fset-ac-le(eq;ac2;ac3))


By

---

Latex:
((Unfold  `fset-ac-le`  0  THEN  Auto)
  THEN  (InstLemma  `fset-all-iff`  [\mkleeneopen{}fset(T)\mkleeneclose{};\mkleeneopen{}deq-fset(eq)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWW  "8"  0  THENA  Auto)
  THEN  (RWW  "8"  7  THENA  Auto)
  THEN  (RWW  "8"  6  THENA  Auto)
  THEN  Thin  8)

---

Home Index