---

Step * of Lemma intersectionset_functionality

∀a,b:coSet{i:l}.  (seteq(a;b) ⇒ seteq(⋂(a);⋂(b)))
BY
{ (Intros
   THEN BLemma `co-seteq-iff`
   THEN Auto
   THEN All (Unfold `intersectionset`)
   THEN (All (RWO "setmem-sub-coset") THENA Auto)
   THEN D -1
   THEN (RWO "3<" 5 ORELSE RWO "3" 5)
   THEN Auto
   THEN (All (RWO "allsetmem-iff") THENA Auto)
   THEN ParallelOp -2
   THEN ParallelLast
   THEN (RWO "3<" 0 ORELSE RWO "3" 0)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,b:coSet\{i:l\}.    (seteq(a;b)  {}\mRightarrow{}  seteq(\mcap{}(a);\mcap{}(b)))


By

---

Latex:
(Intros
  THEN  BLemma  `co-seteq-iff`
  THEN  Auto
  THEN  All  (Unfold  `intersectionset`)
  THEN  (All  (RWO  "setmem-sub-coset")  THENA  Auto)
  THEN  D  -1
  THEN  (RWO  "3<"  5  ORELSE  RWO  "3"  5)
  THEN  Auto
  THEN  (All  (RWO  "allsetmem-iff")  THENA  Auto)
  THEN  ParallelOp  -2
  THEN  ParallelLast
  THEN  (RWO  "3<"  0  ORELSE  RWO  "3"  0)
  THEN  Auto)

---

Home Index