theorem :: IDEAL_1:48

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