Step 
*
 of Lemma 
general_add_com
∀[a:ℤ]. ∀[b:Top].  (a + b ~ b + a)
BY
 
{ Auto }
 
Latex: 
Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[b:Top].    (a  +  b  \msim{}  b  +  a)
 By 
Latex:
Auto
Home
Index