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

proof

assume A2: X is BCK-implicative ; :: thesis: for x, y being Element of X holds y \ (y \ x) = x \ (a \ y)
let x, y be Element of X; :: thesis: y \ (y \ x) = x \ (a \ y)
y \ (y \ x) = x \ (x \ y) by Def1
.= x \ ((a \ y) \ ((a \ y) \ x)) by A1, A2, Th46
.= x \ (x \ (x \ (a \ y))) by Def1 ;
hence y \ (y \ x) = x \ (a \ y) by BCIALG_1:8; :: thesis: verum

end;

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

proof

let x, y be Element of X; :: thesis: (a \ y) \ ((a \ y) \ x) = x \ y
(a \ y) \ ((a \ y) \ x) = x \ (a \ (a \ y)) by A3
.= x \ (y \ (y \ a)) by Def1
.= x \ (y \ (0. X)) by A1 ;
hence (a \ y) \ ((a \ y) \ x) = x \ y by BCIALG_1:2; :: thesis: verum

end;

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