let X be set ; :: thesis: bspace X is add-associative
let x, y, z be Element of (bspace X); :: according to RLVECT_1:def 3 :: thesis: (x + y) + z = x + (y + z)
reconsider A = x, B = y, C = z as Subset of X ;
x + (y + z) = A \+\ (B \+\ C) by Lm1
.= (A \+\ B) \+\ C by XBOOLE_1:91
.= (x + y) + z by Lm1 ;
hence (x + y) + z = x + (y + z) ; :: thesis: verum