theorem Th3: :: IDEAL_1:3

for R being non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr
for I being non empty right-ideal Subset of R holds 0. R in I