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