theorem :: IDEAL_1:47

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