---

Step * 1 2 of Lemma prior-or-latest


1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. Y : EClass(B)
6. Singlevalued(X)
7. Singlevalued(Y)
8. ∀es:EO+(Info). ∀e:E.  (↑e ∈b ((X |- Y))' ⇐⇒ ↑e ∈b ((X)' | (Y)'))
⊢ Singlevalued(((X |- Y))')
BY
{ (ProveSV THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  X  :  EClass(A)
5.  Y  :  EClass(B)
6.  Singlevalued(X)
7.  Singlevalued(Y)
8.  \mforall{}es:EO+(Info).  \mforall{}e:E.    (\muparrow{}e  \mmember{}\msubb{}  ((X  |\msupminus{}  Y))'  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}e  \mmember{}\msubb{}  ((X)'  |  (Y)'))
\mvdash{}  Singlevalued(((X  |\msupminus{}  Y))')


By

---

Latex:
(ProveSV  THEN  Auto)

---

Home Index