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