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 (a \ y) \ ((a \ y) \ x) = x \ 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 (a \ y) \ ((a \ y) \ x) = x \ y ) )

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

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

for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X

( X is BCK-implicative iff for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ 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 (a \ y) \ ((a \ y) \ x) = x \ y ) )

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

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

proof

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

let x, y be Element of X; :: thesis: (a \ y) \ ((a \ y) \ x) = x \ y

X is involutory by A2, Th37;

then A3: x \ (a \ y) = y \ (a \ x) by A1, Th23;

A4: (a \ y) \ ((a \ y) \ x) = x \ (x \ (a \ y)) by Def1;

(y \ (a \ x)) \ y = (y \ y) \ (a \ x) by BCIALG_1:7

.= (a \ x) ` by BCIALG_1:def 5

.= 0. X by BCIALG_1:def 8 ;

then x \ (a \ y) <= y by A3;

then x \ y <= (a \ y) \ ((a \ y) \ x) by A4, BCIALG_1:5;

then A5: (x \ y) \ ((a \ y) \ ((a \ y) \ x)) = 0. X ;

X is BCK-positive-implicative BCK-algebra by A2, Th34;

then a \ y = (a \ y) \ y by Th28;

then ((a \ y) \ ((a \ y) \ x)) \ (x \ y) = 0. X by BCIALG_1:1;

hence (a \ y) \ ((a \ y) \ x) = x \ y by A5, BCIALG_1:def 7; :: thesis: verum

end;let x, y be Element of X; :: thesis: (a \ y) \ ((a \ y) \ x) = x \ y

X is involutory by A2, Th37;

then A3: x \ (a \ y) = y \ (a \ x) by A1, Th23;

A4: (a \ y) \ ((a \ y) \ x) = x \ (x \ (a \ y)) by Def1;

(y \ (a \ x)) \ y = (y \ y) \ (a \ x) by BCIALG_1:7

.= (a \ x) ` by BCIALG_1:def 5

.= 0. X by BCIALG_1:def 8 ;

then x \ (a \ y) <= y by A3;

then x \ y <= (a \ y) \ ((a \ y) \ x) by A4, BCIALG_1:5;

then A5: (x \ y) \ ((a \ y) \ ((a \ y) \ x)) = 0. X ;

X is BCK-positive-implicative BCK-algebra by A2, Th34;

then a \ y = (a \ y) \ y by Th28;

then ((a \ y) \ ((a \ y) \ x)) \ (x \ y) = 0. X by BCIALG_1:1;

hence (a \ y) \ ((a \ y) \ x) = x \ y by A5, BCIALG_1:def 7; :: thesis: verum

for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X

proof

hence
X is BCK-implicative
by A1, Th43; :: thesis: verum
let x be Element of X; :: thesis: (a \ x) \ ((a \ x) \ x) = 0. X

(a \ x) \ ((a \ x) \ x) = x \ x by A6;

hence (a \ x) \ ((a \ x) \ x) = 0. X by BCIALG_1:def 5; :: thesis: verum

end;(a \ x) \ ((a \ x) \ x) = x \ x by A6;

hence (a \ x) \ ((a \ x) \ x) = 0. X by BCIALG_1:def 5; :: thesis: verum