---

Step * 2 1 of Lemma path-comp-union


1. A : SeparationSpace
2. B : SeparationSpace
3. v : Point(A + B)
4. v1 : Point(A + B)
5. v ≡ v1
⊢ (↑isl(v1)) ⇒ (↑isr(v)) ⇒ False
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 RepUR ``ss-eq ss-sep union-ss mk-ss union-sep`` -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{}  (\muparrow{}isl(v1))  {}\mRightarrow{}  (\muparrow{}isr(v))  {}\mRightarrow{}  False


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  RepUR  ``ss-eq  ss-sep  union-ss  mk-ss  union-sep``  -1
  THEN  Auto)

---

Home Index