---

Step * 2 of Lemma isect2_quotient


1. T : Type
2. E1 : T ⟶ T ⟶ ℙ
3. E2 : T ⟶ T ⟶ ℙ
4. EquivRel(T;x,y.E2[x;y])
5. EquivRel(T;x,y.E1[x;y])
⊢ (x,y:T//(E1[x;y] ∧ E2[x;y])) ⊆r x,y:T//E1[x;y] ⋂ x,y:T//E2[x;y]
BY
{ (D 0
   THEN Auto
   THEN Try ((BLemma `equiv_rel_and` THEN Auto))
   THEN (D -1 THENA Auto)
   THEN SqExRepD
   THEN EqTypeCD
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  E1  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  E2  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
4.  EquivRel(T;x,y.E2[x;y])
5.  EquivRel(T;x,y.E1[x;y])
\mvdash{}  (x,y:T//(E1[x;y]  \mwedge{}  E2[x;y]))  \msubseteq{}r  x,y:T//E1[x;y]  \mcap{}  x,y:T//E2[x;y]


By

---

Latex:
(D  0
  THEN  Auto
  THEN  Try  ((BLemma  `equiv\_rel\_and`  THEN  Auto))
  THEN  (D  -1  THENA  Auto)
  THEN  SqExRepD
  THEN  EqTypeCD
  THEN  Auto)\mcdot{}

---

Home Index