---

Step * of Lemma two-intersection-one-intersection

∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List.  (two-intersection(A;W) ⇒ one-intersection(A;W))
BY
{ (Auto
   THEN UnfoldTopAb (-1)
   THEN UnfoldTopAb 0
   THEN (RepeatFor 2 (ParallelLast) THEN InstHyp [⌈i⌉] (-1)⋅ THEN Auto THEN ParallelLast⋅ THEN Auto)⋅) }

---

Latex:


\mforall{}A:Id  List.  \mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List.    (two-intersection(A;W)  {}\mRightarrow{}  one-intersection(A;W))


By

(Auto
  THEN  UnfoldTopAb  (-1)
  THEN  UnfoldTopAb  0
  THEN  (RepeatFor  2  (ParallelLast)  THEN  InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto  THEN  ParallelLast\mcdot{}  THEN  Auto)\mcdot{})

---

Home Index