---

Step * 1 of Lemma imax-list_functionality

.....antecedent..... 
1. L : ℤ List
2. L' : ℤ List
3. 0 < ||L||
4. set-equal(ℤ;L;L')
⊢ l_subset(ℤ;L;L')
BY
{ (Unfold `set-equal` -1 THEN D 0 THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  L  :  \mBbbZ{}  List
2.  L'  :  \mBbbZ{}  List
3.  0  <  ||L||
4.  set-equal(\mBbbZ{};L;L')
\mvdash{}  l\_subset(\mBbbZ{};L;L')


By

---

Latex:
(Unfold  `set-equal`  -1  THEN  D  0  THEN  Auto)

---

Home Index