let X be bounded BCK-algebra; :: thesis: for a being Element of X st a is being_greatest holds
( X is BCK-implicative iff ( X is involutory & X is BCK-positive-implicative ) )
let a be Element of X; :: thesis: ( a is being_greatest implies ( X is BCK-implicative iff ( X is involutory & X is BCK-positive-implicative ) ) )
assume A1: a is being_greatest ; :: thesis: ( X is BCK-implicative iff ( X is involutory & X is BCK-positive-implicative ) )
thus ( X is BCK-implicative implies ( X is involutory & X is BCK-positive-implicative ) ) :: thesis: ( X is involutory & X is BCK-positive-implicative implies X is BCK-implicative )

proof

assume A2: X is BCK-implicative ; :: thesis: ( X is involutory & X is BCK-positive-implicative )
then for a being Element of X st a is being_greatest holds
for x being Element of X holds a \ (a \ x) = x by Lm1;
hence ( X is involutory & X is BCK-positive-implicative ) by A2, Def7, Th34; :: thesis: verum

end;

assume A3: ( X is involutory & X is BCK-positive-implicative ) ; :: 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
A4: (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 ;
y \ a = 0. X by A1, Def2;
then y <= a by BCIALG_1:def 11;
then A5: y \ x <= a \ x by BCIALG_1:5;
x \ (a \ x) = (a \ (a \ x)) \ (a \ x) by A1, A3, Def7
.= a \ (a \ x) by A3, Th28
.= x by A1, A3, Def7 ;
then x <= x \ (y \ x) by A5, BCIALG_1:5;
then x \ (x \ (y \ x)) = 0. X by BCIALG_1:def 11;
hence x \ (y \ x) = x by A4, BCIALG_1:def 7; :: thesis: verum

end;

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