theorem :: IDEAL_1:7

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