---

Step * 1 2 1 of Lemma no-real-separation


1. A : ℝ ⟶ ℙ
2. B : ℝ ⟶ ℙ
3. real-disjoint(x.A[x];y.B[y])
4. x : ℝ
5. A[x]
6. y : ℝ
7. B[y]
8. d : r:ℝ ⟶ (A[r] + B[r])
9. ¬(∃x,y:ℝ. ((x = y) ∧ (↑isl(d x)) ∧ (↑isr(d y))))
10. x1 : ℝ
11. y1 : ℝ
12. x1 = y1
⊢ isl(d x1) = isl(d y1)
BY
{ ((BoolCase ⌜isl(d x1)⌝⋅ THENA Auto)
   THEN (BoolCase ⌜isl(d y1)⌝⋅ THENA Auto)
   THEN ((Fold `member` 0 THEN Auto) ORELSE D 9)) }

1
1. A : ℝ ⟶ ℙ
2. B : ℝ ⟶ ℙ
3. real-disjoint(x.A[x];y.B[y])
4. x : ℝ
5. A[x]
6. y : ℝ
7. B[y]
8. d : r:ℝ ⟶ (A[r] + B[r])
9. x1 : ℝ
10. y1 : ℝ
11. ¬↑isl(d y1)
12. x1 = y1
13. ↑isl(d x1)
⊢ ∃x,y:ℝ. ((x = y) ∧ (↑isl(d x)) ∧ (↑isr(d y)))

2
1. A : ℝ ⟶ ℙ
2. B : ℝ ⟶ ℙ
3. real-disjoint(x.A[x];y.B[y])
4. x : ℝ
5. A[x]
6. y : ℝ
7. B[y]
8. d : r:ℝ ⟶ (A[r] + B[r])
9. x1 : ℝ
10. ¬↑isl(d x1)
11. y1 : ℝ
12. x1 = y1
13. ↑isl(d y1)
⊢ ∃x,y:ℝ. ((x = y) ∧ (↑isl(d x)) ∧ (↑isr(d y)))

---

Latex:

---

Latex:

1.  A  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
2.  B  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
3.  real-disjoint(x.A[x];y.B[y])
4.  x  :  \mBbbR{}
5.  A[x]
6.  y  :  \mBbbR{}
7.  B[y]
8.  d  :  r:\mBbbR{}  {}\mrightarrow{}  (A[r]  +  B[r])
9.  \mneg{}(\mexists{}x,y:\mBbbR{}.  ((x  =  y)  \mwedge{}  (\muparrow{}isl(d  x))  \mwedge{}  (\muparrow{}isr(d  y))))
10.  x1  :  \mBbbR{}
11.  y1  :  \mBbbR{}
12.  x1  =  y1
\mvdash{}  isl(d  x1)  =  isl(d  y1)


By

---

Latex:
((BoolCase  \mkleeneopen{}isl(d  x1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (BoolCase  \mkleeneopen{}isl(d  y1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ((Fold  `member`  0  THEN  Auto)  ORELSE  D  9))

---

Home Index