theorem :: IDEAL_1:49

for L being non empty right_add-cancelable right_zeroed right-distributive left_zeroed doubleLoopStr holds {(0. L)} -LeftIdeal = {(0. L)} by Th45;