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
set a = the Element of I;
(0. R) * the Element of I in I by Def2;
hence 0. R in I by BINOM:1; :: thesis: verum