theorem :: IDEAL_1:52

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