---

Step * of Lemma cut-of-property

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[f:sys-antecedent(es;X)]. ∀[s:fset(E(X))].
  (s ⊆ cut(X;f;s) ∧ (∀[c':Cut(X;f)]. cut(X;f;s) ⊆ c' supposing s ⊆ c'))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `cut-of` 0
   THEN GenConclAtAddr [1;4;1;1;1;1;1]
   THEN GenConclAtAddr [1;4;1]⋅
   THEN D (-2)
   THEN Reduce 0
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[f:sys-antecedent(es;X)].  \mforall{}[s:fset(E(X))].
    (s  \msubseteq{}  cut(X;f;s)  \mwedge{}  (\mforall{}[c':Cut(X;f)].  cut(X;f;s)  \msubseteq{}  c'  supposing  s  \msubseteq{}  c'))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `cut-of`  0
  THEN  GenConclAtAddr  [1;4;1;1;1;1;1]
  THEN  GenConclAtAddr  [1;4;1]\mcdot{}
  THEN  D  (-2)
  THEN  Reduce  0
  THEN  Trivial)

---

Home Index