---

Step * 1 1 2 1 of Lemma implies-member-fset-minimals


1. T : Type
2. eq : EqDecider(T)
3. s : fset(fset(T))
4. a : fset(T)
5. n : ℤ
6. 0 < n
7. ∀a:fset(T)
     (||a|| < n - 1
     ⇒ a ∈ s
     ⇒ (¬(∃z:fset(T). (z ∈ fset-minimals(x,y.f-proper-subset-dec(eq;x;y); s) ∧ z ⊆≠ a)))
     ⇒ a ∈ fset-minimals(x,y.f-proper-subset-dec(eq;x;y); s))
8. a1 : fset(T)
9. ||a1|| < n
10. a1 ∈ s
11. a1 ∈ s
12. y : fset(T)
13. y ∈ s
14. y ⊆≠ a1
15. z : fset(T)
16. z ∈ fset-minimals(x,y.f-proper-subset-dec(eq;x;y); s)
17. z ⊆≠ y
18. z ∈ fset-minimals(x,y.f-proper-subset-dec(eq;x;y); s)
⊢ z ⊆≠ a1
BY
{ (Using [`bs',⌜y⌝] (BLemma `f-proper-subset_transitivity`)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  s  :  fset(fset(T))
4.  a  :  fset(T)
5.  n  :  \mBbbZ{}
6.  0  <  n
7.  \mforall{}a:fset(T)
          (||a||  <  n  -  1
          {}\mRightarrow{}  a  \mmember{}  s
          {}\mRightarrow{}  (\mneg{}(\mexists{}z:fset(T).  (z  \mmember{}  fset-minimals(x,y.f-proper-subset-dec(eq;x;y);  s)  \mwedge{}  z  \msubseteq{}\mneq{}  a)))
          {}\mRightarrow{}  a  \mmember{}  fset-minimals(x,y.f-proper-subset-dec(eq;x;y);  s))
8.  a1  :  fset(T)
9.  ||a1||  <  n
10.  a1  \mmember{}  s
11.  a1  \mmember{}  s
12.  y  :  fset(T)
13.  y  \mmember{}  s
14.  y  \msubseteq{}\mneq{}  a1
15.  z  :  fset(T)
16.  z  \mmember{}  fset-minimals(x,y.f-proper-subset-dec(eq;x;y);  s)
17.  z  \msubseteq{}\mneq{}  y
18.  z  \mmember{}  fset-minimals(x,y.f-proper-subset-dec(eq;x;y);  s)
\mvdash{}  z  \msubseteq{}\mneq{}  a1


By

---

Latex:
(Using  [`bs',\mkleeneopen{}y\mkleeneclose{}]  (BLemma  `f-proper-subset\_transitivity`)\mcdot{}  THEN  Auto)

---

Home Index