Step
*
of Lemma
sg-inv_wf
∀[sg:s-Group]. ∀[x:Point].  (x^-1 ∈ Point)
BY
{ (Auto THEN D 1 THEN Auto THEN ProveWfLemma) }
Latex:
Latex:
\mforall{}[sg:s-Group].  \mforall{}[x:Point].    (x\^{}-1  \mmember{}  Point)
By
Latex:
(Auto  THEN  D  1  THEN  Auto  THEN  ProveWfLemma)
Home
Index