let a, b be Element of L; :: thesis: a *' b = b *' a
thus a *' b = ((a `) + (b `)) `
.= b *' a ; :: thesis: verum