set M = Trivial-addLoopStr ;
thus Trivial-addLoopStr is right_complementable :: according to ALGSTR_0:def 17 :: thesis: Trivial-addLoopStr is left_complementable
proof
let x be Element of Trivial-addLoopStr; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
take x ; :: according to ALGSTR_0:def 11 :: thesis: x + x = 0. Trivial-addLoopStr
thus x + x = 0. Trivial-addLoopStr by STRUCT_0:def 10; :: thesis: verum
end;
let x be Element of Trivial-addLoopStr; :: according to ALGSTR_0:def 15 :: thesis: x is left_complementable
take x ; :: according to ALGSTR_0:def 10 :: thesis: x + x = 0. Trivial-addLoopStr
thus x + x = 0. Trivial-addLoopStr by STRUCT_0:def 10; :: thesis: verum