---

Step * 1 1 1 1 1 of Lemma sys-antecedent-closure


1. Info : Type@i'
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
⊢ ∀f:sys-antecedent(es;X). ((f ∈ []) ⇒ (f ∈ sys-antecedent(es;X)))
BY
{ Obvious }

---

Latex:



1.  Info  :  Type@i'
2.  es  :  EO+(Info)@i'
3.  X  :  EClass(Top)@i'
\mvdash{}  \mforall{}f:sys-antecedent(es;X).  ((f  \mmember{}  [])  {}\mRightarrow{}  (f  \mmember{}  sys-antecedent(es;X)))


By

Obvious

---

Home Index