---

Step * of Lemma es-prior-interface-same

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X,Y:EClass(Top)].
  (∀[e:E]. uiff(↑e ∈b prior(X);↑e ∈b prior(Y))) ∧ (∀[e:E]. prior(Y)(e) = prior(X)(e) ∈ E supposing ↑e ∈b prior(X)) 
  supposing ∀e:E. (↑e ∈b X ⇐⇒ ↑e ∈b Y)
BY
{ (Auto THEN Try (((All (RWO "is-prior-interface") THEN Auto) THEN ParallelLast THEN Complete (Auto)))) }

1
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. Y : EClass(Top)
5. ∀e:E. (↑e ∈b X ⇐⇒ ↑e ∈b Y)
6. ∀[e:E]. uiff(↑e ∈b prior(X);↑e ∈b prior(Y))
7. e : E
8. ↑e ∈b prior(X)
⊢ prior(Y)(e) = prior(X)(e) ∈ E

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X,Y:EClass(Top)].
    (\mforall{}[e:E].  uiff(\muparrow{}e  \mmember{}\msubb{}  prior(X);\muparrow{}e  \mmember{}\msubb{}  prior(Y)))
    \mwedge{}  (\mforall{}[e:E].  prior(Y)(e)  =  prior(X)(e)  supposing  \muparrow{}e  \mmember{}\msubb{}  prior(X)) 
    supposing  \mforall{}e:E.  (\muparrow{}e  \mmember{}\msubb{}  X  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}e  \mmember{}\msubb{}  Y)


By

---

Latex:
(Auto
  THEN  Try  (((All  (RWO  "is-prior-interface")  THEN  Auto)  THEN  ParallelLast  THEN  Complete  (Auto)))
  )

---

Home Index