let X be BCI-algebra; :: thesis: ( ex a being Element of st a is being_greatest implies X is BCK-algebra )
given a being Element of such that A1: a is being_greatest ; :: thesis: X is BCK-algebra
for x being Element of holds x ` = 0. X

proof

let x be Element of ; :: thesis: x ` = 0. X
x \ a = 0. X by A1, Def2;
then x ` = (x \ x) \ a by BCIALG_1:7
.= 0. X by A1, Def2 ;
hence x ` = 0. X ; :: thesis: verum

end;

hence X is BCK-algebra by BCIALG_1:def 8; :: thesis: verum