---

Step * 1 1 1 1 1 of Lemma length-open_box-ge-3


1. X : CubicalSet
2. I : Cname List
3. x : nameset(I)
4. i : ℕ2
5. box : open_box(X;I;[];x;i)
6. 3 < 1 + (||remove-repeats(CnameDeq;[])|| * 2)
7. CnameDeq ∈ EqDecider(nameset(I))
8. 1 < ||remove-repeats(CnameDeq;[])||
9. ¬(∃j1∈[]. (∃j2∈[]. ¬(j1 = j2 ∈ Cname)))
⊢ ∃x:nameset(I). ((x ∈ []) ∧ (∀y:nameset(I). y = x ∈ nameset(I) supposing (y ∈ [])))
BY
{ (Reduce (-2) THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  I  :  Cname  List
3.  x  :  nameset(I)
4.  i  :  \mBbbN{}2
5.  box  :  open\_box(X;I;[];x;i)
6.  3  <  1  +  (||remove-repeats(CnameDeq;[])||  *  2)
7.  CnameDeq  \mmember{}  EqDecider(nameset(I))
8.  1  <  ||remove-repeats(CnameDeq;[])||
9.  \mneg{}(\mexists{}j1\mmember{}[].  (\mexists{}j2\mmember{}[].  \mneg{}(j1  =  j2)))
\mvdash{}  \mexists{}x:nameset(I).  ((x  \mmember{}  [])  \mwedge{}  (\mforall{}y:nameset(I).  y  =  x  supposing  (y  \mmember{}  [])))


By

---

Latex:
(Reduce  (-2)  THEN  Auto)

---

Home Index