---

Step * of Lemma le_int-wf-partial

∀[x,y:partial(Base)].  (x ≤z y ∈ partial(𝔹))
BY
{ ((UnivCD THENA Auto)
   THEN BLemma `base-member-partial`
   THEN Try (Complete (Auto))
   THEN (D 0 THENA Auto)
   THEN Try (Fold `member` 0)
   THEN All (RepUR ``le_int``)
   THEN Try ((HasValueD (-1) THEN RepUR ``bnot ifthenelse`` 0 THEN Auto))) }

1
1. x : partial(Base)
2. y : partial(Base)
3. is-exception(¬by <z x)
⊢ False

---

Latex:

---

Latex:
\mforall{}[x,y:partial(Base)].    (x  \mleq{}z  y  \mmember{}  partial(\mBbbB{}))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  BLemma  `base-member-partial`
  THEN  Try  (Complete  (Auto))
  THEN  (D  0  THENA  Auto)
  THEN  Try  (Fold  `member`  0)
  THEN  All  (RepUR  ``le\_int``)
  THEN  Try  ((HasValueD  (-1)  THEN  RepUR  ``bnot  ifthenelse``  0  THEN  Auto)))

---

Home Index