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 being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X )
let a be Element of X; :: thesis: ( a is being_greatest implies ( X is BCK-implicative iff for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X ) )
assume A1: a is being_greatest ; :: thesis: ( X is BCK-implicative iff for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X )
thus ( X is BCK-implicative implies for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X ) :: thesis: ( ( for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X ) implies X is BCK-implicative )

proof

assume A2: X is BCK-implicative ; :: thesis: for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X
let x be Element of X; :: thesis: (a \ x) \ ((a \ x) \ x) = 0. X
(a \ x) \ ((a \ x) \ x) = x \ (x \ (a \ x)) by Def1
.= x \ x by A2 ;
hence (a \ x) \ ((a \ x) \ x) = 0. X by BCIALG_1:def 5; :: thesis: verum

end;

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

proof

let x, y be Element of X; :: thesis: x \ (y \ x) = x
(a \ x) \ ((a \ x) \ x) = 0. X by A3;
then A4: x \ (x \ (a \ x)) = 0. X by Def1;
y \ a = 0. X by A1;
then y <= a ;
then y \ x <= a \ x by BCIALG_1:5;
then A5: x \ (a \ x) <= x \ (y \ x) by BCIALG_1:5;
(x \ (a \ x)) \ x = (x \ x) \ (a \ x) by BCIALG_1:7
.= (a \ x) ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
then x \ (a \ x) = x by A4, BCIALG_1:def 7;
then A6: x \ (x \ (y \ x)) = 0. X by A5;
(x \ (y \ x)) \ x = (x \ x) \ (y \ x) by BCIALG_1:7
.= (y \ x) ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
hence x \ (y \ x) = x by A6, BCIALG_1:def 7; :: thesis: verum

end;

hence X is BCK-implicative ; :: thesis: verum