let X be BCI-algebra; :: thesis: BCK-part X is p-ideal of X
set A = BCK-part X;
( 0. X in BCK-part X & ( 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 ) )

proof

C1: now

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 B1: ( (x \ z) \ (y \ z) in BCK-part X & y in BCK-part X ) ; :: thesis: x in BCK-part X
then consider d being Element of X such that
B4: ( y = d & 0. X <= d ) ;
B5: y ` = 0. X by B4, BCIALG_1:def 11;
consider c being Element of X such that
B3: ( (x \ z) \ (y \ z) = c & 0. X <= c ) by B1;
((x \ z) \ (y \ z)) ` = 0. X by B3, BCIALG_1:def 11;
then ((x \ z) ` ) \ ((y \ z) ` ) = 0. X by BCIALG_1:9;
then ((x ` ) \ (z ` )) \ ((y \ z) ` ) = 0. X by BCIALG_1:9;
then (((x ` ) \ (z ` )) \ ((0. X) \ (z ` ))) \ ((x ` ) \ (0. X)) = ((x ` ) \ (0. X)) ` by B5, 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 by BCIALG_1:def 11;
hence x in BCK-part X ; :: thesis: verum

end;

(0. X) \ (0. X) = 0. X by BCIALG_1:def 5;
then 0. X <= 0. X by BCIALG_1:def 11;
hence ( 0. X in BCK-part X & ( 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 ) ) by C1; :: thesis: verum

end;

hence BCK-part X is p-ideal of X by Def1; :: thesis: verum