---

Step * of Lemma on-loc-classrel

∀[Info,T:Type]. ∀[X:Id ─→ EClass(T)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:T].  (v ∈ on-loc-class(X)(e) ⇐⇒ v ∈ X loc(e)(e))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``on-loc-class classrel`` 0 THEN MaAuto) }

---

Latex:

---

Latex:
\mforall{}[Info,T:Type].  \mforall{}[X:Id  {}\mrightarrow{}  EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:T].
    (v  \mmember{}  on-loc-class(X)(e)  \mLeftarrow{}{}\mRightarrow{}  v  \mmember{}  X  loc(e)(e))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``on-loc-class  classrel``  0  THEN  MaAuto)

---

Home Index