let a, b be Element of L; :: thesis: a \+\ b = b \+\ a
thus a \+\ b = (a \ b) "\/" (b \ a)
.= b \+\ a ; :: thesis: verum