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

hence ex b_{1} being non empty Subset of X st

( 0. X in b_{1} & ( for x, y, z being Element of X st (x \ y) \ z in b_{1} & z in b_{1} holds

x \ (y \ (y \ x)) in b_{1} ) )
by A1; :: thesis: verum

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

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 ex b

( 0. X in b

x \ (y \ (y \ x)) in b