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