---

Step * 1 of Lemma mk-s-subgroup_wf


1. sg : s-Group
2. P : Point ⟶ ℙ
3. P[1]
4. ∀x:Point. (P[x] ⇒ P[x^-1])
5. ∀x,y:Point.  (P[x] ⇒ P[y] ⇒ P[(x y)])
⊢ set-ss(sg;x.P[x]) ∈ SeparationSpace
BY
{ Auto }

---

Latex:

---

Latex:

1.  sg  :  s-Group
2.  P  :  Point  {}\mrightarrow{}  \mBbbP{}
3.  P[1]
4.  \mforall{}x:Point.  (P[x]  {}\mRightarrow{}  P[x\^{}-1])
5.  \mforall{}x,y:Point.    (P[x]  {}\mRightarrow{}  P[y]  {}\mRightarrow{}  P[(x  y)])
\mvdash{}  set-ss(sg;x.P[x])  \mmember{}  SeparationSpace


By

---

Latex:
Auto

---

Home Index