---

Step * of Lemma l_disjoint_intersection2

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b,c:T List].
  l_disjoint(T;a;l_intersection(eq;b;c)) supposing l_disjoint(T;a;b) ∨ l_disjoint(T;a;c)
BY
{ (Auto
   THEN (RWO "l_disjoint-symmetry" 0 THENA Auto)
   THEN (BLemma `l_disjoint_intersection` THENM ParallelLast THENM BLemma `l_disjoint-symmetry`)
   THEN Auto)⋅ }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[a,b,c:T  List].
    l\_disjoint(T;a;l\_intersection(eq;b;c))  supposing  l\_disjoint(T;a;b)  \mvee{}  l\_disjoint(T;a;c)


By

---

Latex:
(Auto
  THEN  (RWO  "l\_disjoint-symmetry"  0  THENA  Auto)
  THEN  (BLemma  `l\_disjoint\_intersection`  THENM  ParallelLast  THENM  BLemma  `l\_disjoint-symmetry`)
  THEN  Auto)\mcdot{}

---

Home Index