theorem :: IDEAL_1:8

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