---

Step * of Lemma or-latest-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[e:E].
  (X |- Y)(e) = ((X)- | (Y)-)(e) ∈ one_or_both(A;B) supposing (↑e ∈b (X |- Y)) ∧ Singlevalued(X) ∧ Singlevalued(Y)
BY
{ (Auto THEN (RWO "is-or-latest" (-3) THENA Auto)) }

1
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. B : Type
5. X : EClass(A)
6. Y : EClass(B)
7. e : E
8. (↑e ∈b X) ∨ (↑e ∈b Y)
9. Singlevalued(X)
10. Singlevalued(Y)
⊢ (X |- Y)(e) = ((X)- | (Y)-)(e) ∈ one_or_both(A;B)

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[e:E].
    (X  |\msupminus{}  Y)(e)  =  ((X)\msupminus{}  |  (Y)\msupminus{})(e)  supposing  (\muparrow{}e  \mmember{}\msubb{}  (X  |\msupminus{}  Y))  \mwedge{}  Singlevalued(X)  \mwedge{}  Singlevalued(Y)


By

---

Latex:
(Auto  THEN  (RWO  "is-or-latest"  (-3)  THENA  Auto))

---

Home Index