set X1 = BCK-part X;
A1: for x, y, z being Element of X st (x \ y) \ z in BCK-part X & z in BCK-part X holds
x \ (y \ (y \ x)) in BCK-part X

proof

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;

0. X in BCK-part X by BCIALG_1:19;
hence ex b₁ being non empty Subset of X st
( 0. X in b₁ & ( for x, y, z being Element of X st (x \ y) \ z in b₁ & z in b₁ holds
x \ (y \ (y \ x)) in b₁ ) ) by A1; :: thesis: verum