let X be BCI-algebra; :: thesis:
set A = BCK-part X;

let x, y, z be Element of X; :: thesis:
assume that
A2: (x \ z) \ (y \ z) in BCK-part X and
A3: y in BCK-part X ; :: thesis:
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:

end;