let E be non empty Abelian addLoopStr ; :: thesis: for A, B being Subset of E holds A (+) B = B (+) A
let A, B be Subset of E; :: thesis: A (+) B = B (+) A
thus A (+) B = B + A
.= B (+) A ; :: thesis: verum