let X be BCI-algebra; :: thesis: BCK-part X is p-ideal of X

set A = BCK-part X;

then 0. X <= 0. X ;

then 0. X in BCK-part X ;

hence BCK-part X is p-ideal of X by A1, Def5; :: thesis: verum

set A = BCK-part X;

A1: now :: thesis: for x, y, z being Element of X st (x \ z) \ (y \ z) in BCK-part X & y in BCK-part X holds

x in BCK-part X

(0. X) \ (0. X) = 0. X
by BCIALG_1:def 5;x in BCK-part X

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

assume that

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

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

ex c being Element of X st

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

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

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

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

ex d being Element of X st

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

then y ` = 0. X ;

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

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

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

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

then 0. X <= x ;

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

end;assume that

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

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

ex c being Element of X st

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

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

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

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

ex d being Element of X st

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

then y ` = 0. X ;

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

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

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

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

then 0. X <= x ;

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

then 0. X <= 0. X ;

then 0. X in BCK-part X ;

hence BCK-part X is p-ideal of X by A1, Def5; :: thesis: verum