take Y = {(0. X)}; :: thesis: ( Y is Element of K19( the carrier of X) & Y is Ideal of X & Y is associative )

reconsider YY = Y as Ideal of X by BCIALG_1:43;

A1: 0. X in YY by TARSKI:def 1;

for x, y, z being Element of X st x \ (y \ z) in YY & y \ z in YY holds

x = 0. X

x in YY by A1;

hence ( Y is Element of K19( the carrier of X) & Y is Ideal of X & Y is associative ) by A1, Def3; :: thesis: verum

reconsider YY = Y as Ideal of X by BCIALG_1:43;

A1: 0. X in YY by TARSKI:def 1;

for x, y, z being Element of X st x \ (y \ z) in YY & y \ z in YY holds

x = 0. X

proof

then
for x, y, z being Element of X st x \ (y \ z) in YY & y \ z in YY holds
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;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

x in YY by A1;

hence ( Y is Element of K19( the carrier of X) & Y is Ideal of X & Y is associative ) by A1, Def3; :: thesis: verum