theorem :: IDEAL_1:9

for L being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr holds {(0. L)} is RightIdeal of L ;