theorem :: IDEAL_1:50

for L being non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr holds {(0. L)} -RightIdeal = {(0. L)} by Th46;