theorem Th70: :: IDEAL_1:70

for R being non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr
for I being non empty Subset of R holds (0. R) * I = {(0. R)}