take Y = {(0. X)}; :: thesis: ( Y is Element of bool the carrier of X & Y is Ideal of X & Y is associative )
reconsider YY = Y as Ideal of X by BCIALG_1:43;
A1: for x, y, z being Element of X st x \ (y \ z) in YY & y \ z in YY holds
x = 0. X

proof

let x, y, z be Element of X; :: thesis: ( x \ (y \ z) in YY & y \ z in YY implies x = 0. X )
assume ( x \ (y \ z) in YY & y \ z in YY ) ; :: thesis: x = 0. X
then ( x \ (y \ z) = 0. X & y \ z = 0. X ) by TARSKI:def 1;
hence x = 0. X by BCIALG_1:2; :: thesis: verum

end;

A3: ( 0. X in YY & ( for x, y, z being Element of X st x \ (y \ z) in YY & y \ z in YY holds
x = 0. X ) ) by A1, TARSKI:def 1;
( 0. X in YY & ( for x, y, z being Element of X st x \ (y \ z) in YY & y \ z in YY holds
x in YY ) ) by A3;
hence ( Y is Element of bool the carrier of X & Y is Ideal of X & Y is associative ) by Defzzz; :: thesis: verum