let C, M, N be Cardinal; :: thesis: ( C = card (M +^ N) implies C = card (N +^ M) )
assume C = card (M +^ N) ; :: thesis: C = card (N +^ M)
hence C = card H₂(N,M) by Lm1
.= card (N +^ M) by Lm1 ;
:: thesis: verum