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 ;
take x ; :: according to ALGSTR_0:def 11 :: thesis: x + x = 0. (bspace X)
A \+\ A = {} X by XBOOLE_1:92;
hence x + x = 0. (bspace X) by Def5; :: thesis: verum