---

Step * 1 1 of Lemma path-in-union


1. A : SeparationSpace
2. B : SeparationSpace
3. v : Point(A + B)
4. v1 : Point(A + B)
5. v ≡ v1
⊢ isl(v) = isl(v1)
BY
{ (RepUR ``ss-point union-ss mk-ss`` -3
   THEN RepUR ``ss-point union-ss mk-ss`` -2
   THEN D -3
   THEN D -2
   THEN Reduce 0
   THEN ((Fold `member` 0 THEN Auto) ORELSE (RepUR ``ss-eq ss-sep union-ss mk-ss union-sep`` -1 THEN D -1 THEN Auto))) }

---

Latex:

---

Latex:

1.  A  :  SeparationSpace
2.  B  :  SeparationSpace
3.  v  :  Point(A  +  B)
4.  v1  :  Point(A  +  B)
5.  v  \mequiv{}  v1
\mvdash{}  isl(v)  =  isl(v1)


By

---

Latex:
(RepUR  ``ss-point  union-ss  mk-ss``  -3
  THEN  RepUR  ``ss-point  union-ss  mk-ss``  -2
  THEN  D  -3
  THEN  D  -2
  THEN  Reduce  0
  THEN  ((Fold  `member`  0  THEN  Auto)
  ORELSE  (RepUR  ``ss-eq  ss-sep  union-ss  mk-ss  union-sep``  -1  THEN  D  -1  THEN  Auto)
  ))

---

Home Index