theorem lempart0: :: REALALG3:1

for L being non empty right_complementable add-associative right_zeroed addLoopStr holds - {(0. L)} = {(0. L)}