---

Step * of Lemma sub-es-pred_wf

∀[es:EO]. ∀[dom:E ⟶ 𝔹]. ∀[e:E].  (sub-es-pred(es;dom;e) ∈ {e:E| ↑(dom e)} ?)
BY
{ (UniformUnivCD Auto THEN Repeat (MoveToConcl (-1))) }

1
∀es:EO. ∀dom:E ⟶ 𝔹. ∀e:E.  (sub-es-pred(es;dom;e) ∈ {e:E| ↑(dom e)} ?)

---

Latex:

---

Latex:
\mforall{}[es:EO].  \mforall{}[dom:E  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[e:E].    (sub-es-pred(es;dom;e)  \mmember{}  \{e:E|  \muparrow{}(dom  e)\}  ?)


By

---

Latex:
(UniformUnivCD  Auto  THEN  Repeat  (MoveToConcl  (-1)))

---

Home Index