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
consider a being Element of I;
a * (0. R) in I by Def3;
hence 0. R in I by BINOM:2; :: thesis: verum