let X be commutative bounded BCK-algebra; :: thesis: for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) )
let a be Element of X; :: thesis: ( a is being_greatest implies ( X is BCK-implicative iff for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) ) )
assume A1: a is being_greatest ; :: thesis: ( X is BCK-implicative iff for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) )
thus ( X is BCK-implicative implies for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) ) :: thesis: ( ( for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) ) implies X is BCK-implicative )

proof

assume A2: X is BCK-implicative ; :: thesis: for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z)
let x, y, z be Element of X; :: thesis: (x \ (y \ z)) \ (x \ y) <= x \ (a \ z)
X is BCK-positive-implicative BCK-algebra by A2, Th34;
then A3: ((x \ (y \ z)) \ (x \ (x \ z))) \ ((x \ y) \ z) = ((x \ (y \ z)) \ (x \ (x \ z))) \ ((x \ z) \ (y \ z)) by Def11
.= 0. X by BCIALG_1:1 ;
((x \ y) \ z) \ (x \ y) = ((x \ y) \ (x \ y)) \ z by BCIALG_1:7
.= z ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
then A4: ((x \ (y \ z)) \ (x \ (x \ z))) \ (x \ y) = 0. X by A3, BCIALG_1:3;
((x \ (y \ z)) \ (x \ y)) \ (x \ (a \ z)) = ((x \ (y \ z)) \ (x \ y)) \ (z \ (z \ x)) by A1, A2, Th47
.= ((x \ (y \ z)) \ (x \ y)) \ (x \ (x \ z)) by Def1
.= 0. X by A4, BCIALG_1:7 ;
hence (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) ; :: thesis: verum

end;

assume A5: for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) ; :: thesis: X is BCK-implicative
for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X

proof

let x be Element of X; :: thesis: (a \ x) \ ((a \ x) \ x) = 0. X
(x \ (x \ x)) \ (x \ x) <= x \ (a \ x) by A5;
then (x \ (0. X)) \ (x \ x) <= x \ (a \ x) by BCIALG_1:def 5;
then x \ (x \ x) <= x \ (a \ x) by BCIALG_1:2;
then x \ (0. X) <= x \ (a \ x) by BCIALG_1:def 5;
then x <= x \ (a \ x) by BCIALG_1:2;
then x \ (x \ (a \ x)) = 0. X ;
hence (a \ x) \ ((a \ x) \ x) = 0. X by Def1; :: thesis: verum

end;

hence X is BCK-implicative by A1, Th43; :: thesis: verum