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

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