let X be bounded BCK-algebra; :: thesis: ( X is BCK-implicative implies for a being Element of X st a is being_greatest holds
for x being Element of X holds a \ (a \ x) = x )
assume X is BCK-implicative ; :: thesis: for a being Element of X st a is being_greatest holds
for x being Element of X holds a \ (a \ x) = x
then A1: X is commutative BCK-algebra by Th34;
let a be Element of X; :: thesis: ( a is being_greatest implies for x being Element of X holds a \ (a \ x) = x )
assume A2: a is being_greatest ; :: thesis: for x being Element of X holds a \ (a \ x) = x
let x be Element of X; :: thesis: a \ (a \ x) = x
a \ (a \ x) = x \ (x \ a) by A1, Def1
.= x \ (0. X) by A2 ;
hence a \ (a \ x) = x by BCIALG_1:2; :: thesis: verum