let R be non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr ; :: thesis: for I being non empty right-ideal Subset of holds 0. R in I
let I be non empty right-ideal Subset of ; :: 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