---

Step * of Lemma cut-order_transitivity

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[f:sys-antecedent(es;X)]. ∀[a,b,c:E(X)].
  (a ≤(X;f) c) supposing (b ≤(X;f) c and a ≤(X;f) b)
BY
{ (Auto THEN All (\h. Unfold `cut-order` h)⋅ THEN Assert ⌈cut(X;f;{b}) ⊆ cut(X;f;{c})⌉⋅) }

1
.....assertion..... 
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. f : sys-antecedent(es;X)
5. a : E(X)
6. b : E(X)
7. c : E(X)
8. a ∈ cut(X;f;{b})
9. b ∈ cut(X;f;{c})
⊢ cut(X;f;{b}) ⊆ cut(X;f;{c})

2
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. f : sys-antecedent(es;X)
5. a : E(X)
6. b : E(X)
7. c : E(X)
8. a ∈ cut(X;f;{b})
9. b ∈ cut(X;f;{c})
10. cut(X;f;{b}) ⊆ cut(X;f;{c})
⊢ a ∈ cut(X;f;{c})

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[f:sys-antecedent(es;X)].  \mforall{}[a,b,c:E(X)].
    (a  \mleq{}(X;f)  c)  supposing  (b  \mleq{}(X;f)  c  and  a  \mleq{}(X;f)  b)


By

---

Latex:
(Auto  THEN  All  (\mbackslash{}h.  Unfold  `cut-order`  h)\mcdot{}  THEN  Assert  \mkleeneopen{}cut(X;f;\{b\})  \msubseteq{}  cut(X;f;\{c\})\mkleeneclose{}\mcdot{})

---

Home Index