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

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

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

let x, y be Element of X; :: according to BCIALG_3:def 12 :: thesis: x \ (y \ x) = x

(a \ x) \ ((a \ x) \ x) = (a \ x) \ (a \ x) by A4

.= 0. X by BCIALG_1:def 5 ;

then A5: 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 A6: 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 A5, BCIALG_1:def 7;

then A7: x \ (x \ (y \ x)) = 0. X by A6;

(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 A7, BCIALG_1:def 7; :: thesis: verum

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

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

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

proof

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

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

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

.= x ` by BCIALG_1:def 5

.= 0. X by BCIALG_1:def 8 ;

(a \ x) \ ((a \ x) \ x) = 0. X by A1, A2, Th43;

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

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

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

.= x ` by BCIALG_1:def 5

.= 0. X by BCIALG_1:def 8 ;

(a \ x) \ ((a \ x) \ x) = 0. X by A1, A2, Th43;

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

let x, y be Element of X; :: according to BCIALG_3:def 12 :: thesis: x \ (y \ x) = x

(a \ x) \ ((a \ x) \ x) = (a \ x) \ (a \ x) by A4

.= 0. X by BCIALG_1:def 5 ;

then A5: 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 A6: 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 A5, BCIALG_1:def 7;

then A7: x \ (x \ (y \ x)) = 0. X by A6;

(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 A7, BCIALG_1:def 7; :: thesis: verum