let R be non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr ; :: thesis: for I being non empty right-ideal Subset of R holds 0. R in I
let I be non empty right-ideal Subset of R; :: thesis: 0. R in I
set a = the Element of I;
the Element of I * (0. R) in I by Def3;
hence 0. R in I by BINOM:2; :: thesis: verum