Step
*
of Lemma
mcomp_imp_not_unit
∀g:IAbMonoid. ∀a:|g|.  (Reducible(a) 
⇒ (¬(g-unit(a))))
BY
{ UnivCD THENA Auto }
1
1. g : IAbMonoid
2. a : |g|
3. Reducible(a)
⊢ ¬(g-unit(a))
Latex:
Latex:
\mforall{}g:IAbMonoid.  \mforall{}a:|g|.    (Reducible(a)  {}\mRightarrow{}  (\mneg{}(g-unit(a))))
By
Latex:
UnivCD  THENA  Auto
Home
Index