---

Step * of Lemma equiv_rel_isect2

∀[A,B:Type].  ∀E:A ⟶ A ⟶ ℙ. (EquivRel(A;x,y.E[x;y]) ⇒ EquivRel(A ⋂ B;x,y.E[x;y]))
BY
{ (Auto THEN InstLemma `equiv_rel_subtype` [⌜A⌝;⌜A ⋂ B⌝;⌜E⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    \mforall{}E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}.  (EquivRel(A;x,y.E[x;y])  {}\mRightarrow{}  EquivRel(A  \mcap{}  B;x,y.E[x;y]))


By

---

Latex:
(Auto  THEN  InstLemma  `equiv\_rel\_subtype`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}A  \mcap{}  B\mkleeneclose{};\mkleeneopen{}E\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index