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

proof

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

end;

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