let R be non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr ; :: thesis: for I being non empty left-ideal Subset of R holds 0. R in I
let I be non empty left-ideal Subset of R; :: thesis: 0. R in I
consider a being Element of I;
(0. R) * a in I by Def2;
hence 0. R in I by BINOM:1; :: thesis: verum