---

Step * of Lemma set-part-greatest

∀s:coSet{i:l}. ((set-part(s) ⊆ s) ∧ (∀x:Set{i:l}. ((x ⊆ s) ⇒ (x ⊆ set-part(s)))))
BY
{ Auto }

1
1. s : coSet{i:l}
⊢ (set-part(s) ⊆ s)

2
1. s : coSet{i:l}
2. (set-part(s) ⊆ s)
3. x : Set{i:l}
4. (x ⊆ s)
⊢ (x ⊆ set-part(s))

---

Latex:

---

Latex:
\mforall{}s:coSet\{i:l\}.  ((set-part(s)  \msubseteq{}  s)  \mwedge{}  (\mforall{}x:Set\{i:l\}.  ((x  \msubseteq{}  s)  {}\mRightarrow{}  (x  \msubseteq{}  set-part(s)))))


By

---

Latex:
Auto

---

Home Index