let X be BCK-algebra; :: thesis: BCK-part X is commutative Ideal of X

set B = BCK-part X;

A1: for x, y being Element of X st x \ y in BCK-part X & y in BCK-part X holds

x in BCK-part X

x \ (y \ (y \ x)) in BCK-part X

hence BCK-part X is commutative Ideal of X by A1, A5, Def6, BCIALG_1:def 18; :: thesis: verum

set B = BCK-part X;

A1: for x, y being Element of X st x \ y in BCK-part X & y in BCK-part X holds

x in BCK-part X

proof

A5:
for x, y, z being Element of X st (x \ y) \ z in BCK-part X & z in BCK-part X holds
let x, y be Element of X; :: thesis: ( x \ y in BCK-part X & y in BCK-part X implies x in BCK-part X )

assume that

A2: x \ y in BCK-part X and

A3: y in BCK-part X ; :: thesis: x in BCK-part X

ex x1 being Element of X st

( x \ y = x1 & 0. X <= x1 ) by A2;

then (x \ y) ` = 0. X ;

then A4: (x `) \ (y `) = 0. X by BCIALG_1:9;

ex x2 being Element of X st

( y = x2 & 0. X <= x2 ) by A3;

then (x `) \ (0. X) = 0. X by A4;

then (0. X) \ x = 0. X by BCIALG_1:2;

then 0. X <= x ;

hence x in BCK-part X ; :: thesis: verum

end;assume that

A2: x \ y in BCK-part X and

A3: y in BCK-part X ; :: thesis: x in BCK-part X

ex x1 being Element of X st

( x \ y = x1 & 0. X <= x1 ) by A2;

then (x \ y) ` = 0. X ;

then A4: (x `) \ (y `) = 0. X by BCIALG_1:9;

ex x2 being Element of X st

( y = x2 & 0. X <= x2 ) by A3;

then (x `) \ (0. X) = 0. X by A4;

then (0. X) \ x = 0. X by BCIALG_1:2;

then 0. X <= x ;

hence x in BCK-part X ; :: thesis: verum

x \ (y \ (y \ x)) in BCK-part X

proof

0. X in BCK-part X
by BCIALG_1:19;
let x, y, z be Element of X; :: thesis: ( (x \ y) \ z in BCK-part X & z in BCK-part X implies x \ (y \ (y \ x)) in BCK-part X )

assume that

(x \ y) \ z in BCK-part X and

z in BCK-part X ; :: thesis: x \ (y \ (y \ x)) in BCK-part X

(0. X) \ (x \ (y \ (y \ x))) = (x \ (y \ (y \ x))) `

.= 0. X by BCIALG_1:def 8 ;

then 0. X <= x \ (y \ (y \ x)) ;

hence x \ (y \ (y \ x)) in BCK-part X ; :: thesis: verum

end;assume that

(x \ y) \ z in BCK-part X and

z in BCK-part X ; :: thesis: x \ (y \ (y \ x)) in BCK-part X

(0. X) \ (x \ (y \ (y \ x))) = (x \ (y \ (y \ x))) `

.= 0. X by BCIALG_1:def 8 ;

then 0. X <= x \ (y \ (y \ x)) ;

hence x \ (y \ (y \ x)) in BCK-part X ; :: thesis: verum

hence BCK-part X is commutative Ideal of X by A1, A5, Def6, BCIALG_1:def 18; :: thesis: verum