---

Step * of Lemma latest-val-cases

∀[Info:Type]
  ∀es:EO+(Info)
    ∀[T:Type]
      ∀X:EClass(T). ∀e:E.
        (↑e ∈b (X)- ⇐⇒ ((↑e ∈b X) ∧ ((X)-(e) = X(e) ∈ T)) ∨ (((↑e ∈b (X)') ∧ (¬↑e ∈b X)) ∧ ((X)-(e) = (X)'(e) ∈ T)))
BY
{ (UnivCD THENA Auto) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. [T] : Type
4. X : EClass(T)@i'
5. e : E@i
⊢ ↑e ∈b (X)- ⇐⇒ ((↑e ∈b X) ∧ ((X)-(e) = X(e) ∈ T)) ∨ (((↑e ∈b (X)') ∧ (¬↑e ∈b X)) ∧ ((X)-(e) = (X)'(e) ∈ T))

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[T:Type]
            \mforall{}X:EClass(T).  \mforall{}e:E.
                (\muparrow{}e  \mmember{}\msubb{}  (X)\msupminus{}
                \mLeftarrow{}{}\mRightarrow{}  ((\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  ((X)\msupminus{}(e)  =  X(e)))  \mvee{}  (((\muparrow{}e  \mmember{}\msubb{}  (X)')  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  X))  \mwedge{}  ((X)\msupminus{}(e)  =  (X)'(e))))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index