let X be BCK-algebra; :: thesis: for IT being non empty Subset of X
for X being BCK-algebra st IT is Commutative-Ideal of X holds
IT is Ideal of X
let IT be non empty Subset of X; :: thesis: for X being BCK-algebra st IT is Commutative-Ideal of X holds
IT is Ideal of X
let X be BCK-algebra; :: thesis: ( IT is Commutative-Ideal of X implies IT is Ideal of X )
assume A1: IT is Commutative-Ideal of X ; :: thesis: IT is Ideal of X
A2: for x, y being Element of X st x \ y in IT & y in IT holds
x in IT

proof

let x, y be Element of X; :: thesis: ( x \ y in IT & y in IT implies x in IT )
assume that
A3: x \ y in IT and
A4: y in IT ; :: thesis: x in IT
A5: x \ ((0. X) \ ((0. X) \ x)) = x \ ((0. X) \ (x `))
.= x \ ((0. X) \ (0. X)) by BCIALG_1:def 8
.= x \ (0. X) by BCIALG_1:def 5
.= x by BCIALG_1:2 ;
(x \ (0. X)) \ y in IT by A3, BCIALG_1:2;
hence x in IT by A1, A4, A5, Def10; :: thesis: verum

end;

0. X in IT by A1, Def10;
hence IT is Ideal of X by A1, A2, BCIALG_1:def 18; :: thesis: verum