let L be non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr ; :: thesis: {(0. L)} is left-ideal
let p, x be Element of L; :: according to IDEAL_1:def 2 :: thesis: ( x in {(0. L)} implies p * x in {(0. L)} )
reconsider p9 = p as Element of L ;
assume x in {(0. L)} ; :: thesis: p * x in {(0. L)}
then x = 0. L by TARSKI:def 1;
then p9 * x = 0. L by BINOM:2;
hence p * x in {(0. L)} by TARSKI:def 1; :: thesis: verum