---

Step * 2 1 of Lemma continuous-monotone-co-value


1. S : Type
2. c : (S × S) ⋃ (S + S)
⊢ (↑is-atomic(c)) ⇒ False
BY
{ (D_b_union (-1)
   THEN Try ((D -1 THEN RepUR ``is-atomic`` 0))
   THEN Auto
   THEN D -2
   THEN RepUR ``is-atomic`` -1
   THEN Auto) }

---

Latex:

---

Latex:

1.  S  :  Type
2.  c  :  (S  \mtimes{}  S)  \mcup{}  (S  +  S)
\mvdash{}  (\muparrow{}is-atomic(c))  {}\mRightarrow{}  False


By

---

Latex:
(D\_b\_union  (-1)
  THEN  Try  ((D  -1  THEN  RepUR  ``is-atomic``  0))
  THEN  Auto
  THEN  D  -2
  THEN  RepUR  ``is-atomic``  -1
  THEN  Auto)

---

Home Index