let X be set ; :: thesis: bspace X is right_complementable
let x be Element of (bspace X); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider A = x as Subset of X ;
A1: A \+\ A = {} X by XBOOLE_1:92;
take x ; :: according to ALGSTR_0:def 11 :: thesis: x + x = 0. (bspace X)
thus x + x = 0. (bspace X) by A1, Def5; :: thesis: verum