---

Step * of Lemma length-open_box_image

∀[X,I,K,f,bx:Top].  (||open_box_image(X;I;K;f;bx)|| ~ ||bx||)
BY
{ (Intros THEN RepUR ``open_box_image`` 0 THEN RWO "map-length" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X,I,K,f,bx:Top].    (||open\_box\_image(X;I;K;f;bx)||  \msim{}  ||bx||)


By

---

Latex:
(Intros  THEN  RepUR  ``open\_box\_image``  0  THEN  RWO  "map-length"  0  THEN  Auto)

---

Home Index