for L being non empty left_unital doubleLoopStr holds {(1. L)} -RightIdeal = the carrier of L