let X be set ; :: thesis: bspace X is Abelian
let x, y be Element of (bspace X); :: according to RLVECT_1:def 2 :: thesis: x + y = y + x
reconsider A = x, B = y as Subset of X ;
x + y = B \+\ A by Def5
.= y + x by Def5 ;
hence x + y = y + x ; :: thesis: verum