theorem Th2: :: IDEAL_1:2

for R being non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr
for I being non empty left-ideal Subset of R holds 0. R in I