---

Step * of Lemma disjoint-classrel-symm

∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)].
  (disjoint-classrel(es;B;Y;A;X) ⇒ disjoint-classrel(es;A;X;B;Y))
BY
{ ((UnivCD THENA Auto)
   THEN All (Unfold `disjoint-classrel`)⋅
   THEN Auto
   THEN (InstHyp [⌈e⌉] (-2)⋅ THENA Auto)
   THEN D (-1)
   THEN Auto) }

---

Latex:


\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[es:EO+(Info)].
    (disjoint-classrel(es;B;Y;A;X)  {}\mRightarrow{}  disjoint-classrel(es;A;X;B;Y))


By

((UnivCD  THENA  Auto)
  THEN  All  (Unfold  `disjoint-classrel`)\mcdot{}
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Auto)

---

Home Index